1  /-
  2  Copyright (c) 2018 Mario Carneiro. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Mario Carneiro, Johannes Hölzl
  5  
  6  Lebesgue integral on `ennreal`.
  7  
  8  We define simple functions and show that each Borel measurable function on `ennreal` can be
  9  approximated by a sequence of simple functions.
 10  -/
 11  import
 12    algebra.pi_instances
src    └──────────────────┘
 13    measure_theory.measure_space
src    └──────────────────────────┘
 14    measure_theory.borel_space
src    └────────────────────────┘
 15  noncomputable theory
 16  open lattice set filter
 17  open_locale classical topological_space
 18  
 19  namespace measure_theory
 20  
 21  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 22  
 23  /-- A function `f` from a measurable space to any type is called *simple*,
 24  if every preimage `f ⁻¹' {x}` is measurable, and the range is finite. This structure bundles
 25  a function with these properties. -/
 26  structure {u v} simple_func (α : Type u) [measurable_space α] (β : Type v) :=
 27  (to_fun : α → β)
 28  (measurable_sn : ∀ x, is_measurable (to_fun ⁻¹' {x}))
id                        └───────────┘  └────┘ └─┘ 
src                        └───────────┘         └─┘ 
typ                       └───────────┘  └────┘ └─┘ 
doc                        └───────────┘         └─┘
 29  (finite : (set.range to_fun).finite)
id              └───────┘ └────┘ └────┘
src             └───────┘        └────┘
typ             └───────┘ └────┘ └────┘
doc             └───────┘        └────┘
 30  
 31  local infixr ` →ₛ `:25 := simple_func
id                             └─────────┘
src                            └─────────┘
typ                            └─────────┘
doc                            └─────────┘
 32  
 33  namespace simple_func
 34  
 35  section measurable
 36  variables [measurable_space α]
id              └──────────────┘
src             └──────────────┘
typ             └──────────────┘
 37  instance has_coe_to_fun : has_coe_to_fun (α →ₛ β) := ⟨_, to_fun⟩
id                             └────────────┘   └┘          └────┘
src                            └────────────┘    └┘           └────┘
typ                            └────────────┘   └┘          └────┘
doc                                              └┘
 38  
 39  @[ext] theorem ext {f g : α →ₛ β} (H : ∀ a, f a = g a) : f = g :=
id                              └┘                      
src                              └┘                            
typ                             └┘                      
doc    └─┘                       └┘
 40  by cases f; cases g; congr; exact funext H
id                                   └────┘ 
src     └────┘   └────┘   └───┘  └────┘└────┘ 
typ     └────┘  └────┘  └───┘  └────┘└────┘
doc     └────┘   └────┘          └────┘       
txt     └────┘   └────┘   └───┘  └────┘       
par     └────┘   └────┘   └───┘  └────┘       
pid                                        
st     └────────────────────────────────────────
 41  
src  
typ  
doc  
txt  
par  
pid  
st   
 42  /-- Range of a simple function `α →ₛ β` as a `finset β`. -/
 43  protected def range (f : α →ₛ β) : finset β := f.finite.to_finset
id                             └┘     └────┘     └─────┘└────────┘
src                             └┘      └────┘       └─────┘└────────┘
typ                            └┘     └────┘     └─────┘└────────┘
doc                             └┘      └────┘              └────────┘
 44  
 45  @[simp] theorem mem_range {f : α →ₛ β} {b} : b ∈ f.range ↔ ∃ a, f a = b :=
id                                   └┘           └────┘       
src                                   └┘              └────┘         
typ                                  └┘           └────┘       
doc    └──┘                           └┘               └────┘
 46  finite.mem_to_finset
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
 47  
 48  lemma preimage_eq_empty_iff (f : α →ₛ β) (b : β) : f ⁻¹' {b} = ∅ ↔ b ∉ f.range :=
id                                     └┘             └─┘        └────┘
src                                     └┘                └─┘           └────┘
typ                                    └┘             └─┘        └────┘
doc                                     └┘                └─┘                └────┘
 49  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
 50    (by simp [set.eq_empty_iff_forall_not_mem, mem_range])
id               └─────────────────────────────┘  └───────┘
src        └────┘└─────────────────────────────┘└┘└───────┘
typ        └────┘└─────────────────────────────┘└┘└───────┘
doc        └────┘                               └┘         
txt        └────┘                               └┘         
par        └────┘                               └┘         
pid                                           └┘         
st        └────────────────────────────────────────────────┘
 51    (by simp [set.eq_empty_iff_forall_not_mem, mem_range])
id               └─────────────────────────────┘  └───────┘
src        └────┘└─────────────────────────────┘└┘└───────┘
typ        └────┘└─────────────────────────────┘└┘└───────┘
doc        └────┘                               └┘         
txt        └────┘                               └┘         
par        └────┘                               └┘         
pid                                           └┘         
st        └────────────────────────────────────────────────┘
 52  
 53  /-- Constant function as a `simple_func`. -/
 54  def const (α) {β} [measurable_space α] (b : β) : α →ₛ β :=
id                      └──────────────┘             └┘ 
src                     └──────────────┘                └┘
typ                     └──────────────┘             └┘ 
doc                                                     └┘
 55  ⟨λ a, b, λ x, is_measurable.const _,
id              └─────────────────┘
src                └─────────────────┘
typ             └─────────────────┘
 56    finite_subset (set.finite_singleton b) $ by rintro _ ⟨a, rfl⟩; simp⟩
id     └───────────┘  └──────────────────┘ 
src    └───────────┘  └──────────────────┘         └───────────────┘  └──┘
typ    └───────────┘  └──────────────────┘        └───────────────┘  └──┘
doc                                                └───────────────┘  └──┘
txt                                                └───────────────┘  └──┘
par                                                └───────────────┘  └──┘
pid                                                      └─────────┘
st                                                └──────────────────────┘
 57  
 58  instance [inhabited β] : inhabited (α →ₛ β) := ⟨const _ (default _)⟩
id             └───────┘     └───────┘   └┘       └───┘    └─────┘
src            └───────┘      └───────┘    └┘        └───┘    └─────┘
typ            └───────┘     └───────┘   └┘       └───┘    └─────┘
doc                                        └┘        └───┘
 59  
 60  @[simp] theorem const_apply (a : α) (b : β) : (const α b) a = b := rfl
id                                                └───┘          └─┘
src                                                 └───┘              └─┘
typ                                               └───┘          └─┘
doc    └──┘                                         └───┘
 61  
 62  lemma range_const (α) [measurable_space α] [ne : nonempty α] (b : β) :
id                          └──────────────┘         └──────┘        
src                         └──────────────┘          └──────┘
typ                         └──────────────┘         └──────┘        
 63    (const α b).range = {b} :=
id      └───┘   └───┘   
src     └───┘     └───┘   
typ     └───┘   └───┘   
doc     └───┘     └───┘
 64  begin
st   └─────
 65    ext b',
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid       └─┘
st   ───────┘└─
 66    simp [mem_range],
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                 
st   ─────────────────┘└─
 67    exact ⟨assume ⟨_, h⟩, h.symm, assume h, ne.elim $ λa, ⟨a, h.symm⟩⟩
id                           └───┘            └─────┘            └───┘
src    └────┘       └───┘ └─┘ └───┘└┘      └──┘└─────┘  └─┘  └┘ └───┘└─┘
typ    └────┘       └───┘└─┘ └───┘└┘      └──┘└─────┘  └─┘  └┘ └───┘└─┘
doc    └────┘       └───┘ └─┘      └┘      └──┘         └─┘  └┘      └─┘
txt    └────┘       └───┘ └─┘      └┘      └──┘         └─┘  └┘      └─┘
par    └────┘       └───┘ └─┘      └┘      └──┘         └─┘  └┘      └─┘
pid                └───┘ └─┘      └┘      └──┘         └─┘  └┘      └┘
st   ────────────────────────────────────────────────────────────────────┘
 68  end
st   └─┘
 69  
 70  lemma is_measurable_cut (p : α → β → Prop) (f : α →ₛ β)
id                                                  └┘ 
src                                                    └┘
typ                                                 └┘ 
doc                                                    └┘
 71    (h : ∀b, is_measurable {a | p a b}) : is_measurable {a | p a (f a)} :=
id             └───────────┘           └───────────┘        
src             └───────────┘               └───────────┘ 
typ            └───────────┘           └───────────┘        
doc             └───────────┘                └───────────┘
 72  begin
st   └─────
 73    rw (_ : {a | p a (f a)} = ⋃ b ∈ set.range f, {a | p a b} ∩ f ⁻¹' {b}),
id                                   └───────┘               └─┘ 
src    └─┘ └──┘ └──┘     └─┘└───┘└───────┘ └──┘   └┘ └─┘└─┘
typ    └─┘ └──┘ └──┘     └─┘└───┘└───────┘ └──┘  └┘└─┘└─┘
doc    └─┘ └──┘ └──┘     └─┘ └───┘└───────┘  └──┘   └┘  └─┘ └─┘
txt    └─┘ └──┘ └──┘     └─┘  └───┘            └──┘   └┘      └─┘
par    └─┘ └──┘ └──┘     └─┘  └───┘            └──┘   └┘      └─┘
pid       └──┘ └──┘     └─┘  └───┘            └──┘   └┘      └─┘
st   ──────────────────────────────────────────────────────────────────────┘└─
 74    { exact is_measurable.bUnion (countable_finite f.finite)
id             └──────────────────┘  └──────────────┘ └──────┘
src      └────┘└──────────────────┘ └──────────────┘└──────┘└─
typ      └────┘└──────────────────┘ └──────────────┘└──────┘└─
doc      └────┘                                             └─
txt      └────┘                                             └─
par      └────┘                                             └─
pid                                                        └─
st   ───┘└──────────────────────────────────────────────────────
 75        (λ b _, is_measurable.inter (h b) (f.measurable_sn _)) },
id                 └─────────────────┘       └─────────────┘
src  ─────┘  └────┘└─────────────────┘   └┘ └─────────────┘└───┘
typ  ─────┘  └────┘└─────────────────┘  └┘ └─────────────┘└───┘
doc  ─────┘  └────┘                      └┘                └───┘
txt  ─────┘  └────┘                      └┘                └───┘
par  ─────┘  └────┘                      └┘                └───┘
pid  ─────┘  └────┘                      └┘                └──┘
st   ────────────────────────────────────────────────────────────┘└┘
 76    ext a, simp,
src    └───┘  └──┘
typ    └───┘  └──┘
doc    └───┘  └──┘
txt    └───┘  └──┘
par    └───┘  └──┘
pid       └┘
st   ──────┘└────┘└─
 77    exact ⟨λ h, ⟨_, ⟨a, rfl⟩, h, rfl⟩, λ ⟨_, ⟨a', rfl⟩, h', e⟩, e.symm ▸ h'⟩
id                                 └─┘                    └┘      └───┘ 
src    └────┘  └──┘ └─┘  └┘   └─┘ └┘└─┘└─┘ └───┘   └┘   └─┘  └┘ └─┘ └───┘  └┘
typ    └────┘  └──┘ └─┘ └┘   └─┘ └┘└─┘└─┘ └───┘   └┘   └─┘└┘└┘└─┘ └───┘  └┘
doc    └────┘  └──┘ └─┘  └┘   └─┘ └┘   └─┘ └───┘   └┘   └─┘  └┘ └─┘         └┘
txt    └────┘  └──┘ └─┘  └┘   └─┘ └┘   └─┘ └───┘   └┘   └─┘  └┘ └─┘         └┘
par    └────┘  └──┘ └─┘  └┘   └─┘ └┘   └─┘ └───┘   └┘   └─┘  └┘ └─┘         └┘
pid           └──┘ └─┘  └┘   └─┘ └┘   └─┘ └───┘   └┘   └─┘  └┘ └─┘         
st   ──────────────────────────────────────────────────────────────────────────┘
 78  end
st   └─┘
 79  
 80  theorem preimage_measurable (f : α →ₛ β) (s) : is_measurable (f ⁻¹' s) :=
id                                     └┘         └───────────┘   └─┘ 
src                                     └┘          └───────────┘    └─┘
typ                                    └┘         └───────────┘   └─┘ 
doc                                     └┘          └───────────┘    └─┘
 81  is_measurable_cut (λ _ b, b ∈ s) f (λ b, by simp [is_measurable.const])
id   └───────────────┘                          └─────────────────┘
src  └───────────────┘                          └────┘└─────────────────┘
typ  └───────────────┘                    └────┘└─────────────────┘
doc                                              └────┘                   
txt                                              └────┘                   
par                                              └────┘                   
pid                                                                     
st                                              └─────────────────────────┘
 82  
 83  /-- A simple function is measurable -/
 84  theorem measurable [measurable_space β] (f : α →ₛ β) : measurable f :=
id                       └──────────────┘         └┘     └────────┘ 
src                      └──────────────┘           └┘      └────────┘
typ                      └──────────────┘         └┘     └────────┘ 
doc                                                 └┘      └────────┘
 85  λ s _, preimage_measurable f s
id        └─────────────────┘  
src         └─────────────────┘
typ       └─────────────────┘  
 86  
 87  def ite {s : set α} (hs : is_measurable s) (f g : α →ₛ β) : α →ₛ β :=
id                └─┘         └───────────┘           └┘      └┘ 
src               └─┘          └───────────┘             └┘        └┘
typ               └─┘         └───────────┘           └┘      └┘ 
doc                            └───────────┘             └┘        └┘
 88  ⟨λ a, if a ∈ s then f a else g a,
id                           
src             
typ                          
 89   λ x, by letI : measurable_space β := ⊤; exact
id                  └──────────────┘     
src           └─────┘└──────────────┘ └──┘  └─────
typ          └─────┘└──────────────┘└──┘  └─────
doc           └─────┘                 └──┘   └─────
txt           └─────┘                 └──┘   └─────
par           └─────┘                 └──┘   └─────
pid               └┘                 └──┘        
st           └──────────────────────────────────────
 90     measurable.if hs f.measurable g.measurable _ trivial,
id      └───────────┘ └┘ └──────────┘ └──────────┘   └─────┘
src  ──┘└───────────┘  └──────────┘└──────────┘└─┘└─────┘
typ  ──┘└───────────┘└┘└──────────┘└──────────┘└─┘└─────┘
doc  ──┘               └──────────┘└──────────┘└─┘
txt  ──┘                                       └─┘
par  ──┘                                       └─┘
pid  ──┘                                       └─┘
st   ──────────────────────────────────────────────────────┘
 91   finite_subset (finite_union f.finite g.finite) begin
id    └───────────┘  └──────────┘ └─────┘ └─────┘
src   └───────────┘  └──────────┘  └─────┘  └─────┘
typ   └───────────┘  └──────────┘ └─────┘ └─────┘
st                                                   └─────
 92     rintro _ ⟨a, rfl⟩,
src     └───────────────┘
typ     └───────────────┘
doc     └───────────────┘
txt     └───────────────┘
par     └───────────────┘
pid           └─────────┘
st   ───────────────────┘└─
 93     by_cases a ∈ s; simp [h],
id                         
src     └───────┘    └────┘ 
typ     └───────┘  └────┘
doc     └───────┘     └────┘ 
txt     └───────┘     └────┘ 
par     └───────┘     └────┘ 
pid                       
st   ──────────────────────────┘└─
 94     exacts [or.inl ⟨_, rfl⟩, or.inr ⟨_, rfl⟩]
id              └────┘     └─┘   └────┘     └─┘
src     └──────┘└────┘ └─┘└─┘└─┘└────┘ └─┘└─┘└──
typ     └──────┘└────┘ └─┘└─┘└─┘└────┘ └─┘└─┘└──
doc     └──────┘       └─┘   └─┘       └─┘   └──
txt     └──────┘       └─┘   └─┘       └─┘   └──
par     └──────┘       └─┘   └─┘       └─┘   └──
pid           └┘       └─┘   └─┘       └─┘   └┘
st   ─────────────────────────────────────────────
 95   end⟩
src  
typ  
doc  
txt  
par  
pid  
st   └─┘
 96  
 97  @[simp] theorem ite_apply {s : set α} (hs : is_measurable s)
id                                  └─┘         └───────────┘ 
src                                 └─┘          └───────────┘
typ                                 └─┘         └───────────┘ 
doc    └──┘                                      └───────────┘
 98    (f g : α →ₛ β) (a) : ite hs f g a = if a ∈ s then f a else g a := rfl
id             └┘         └─┘ └┘                            └─┘
src             └┘          └─┘                                        └─┘
typ            └┘         └─┘ └┘                            └─┘
doc             └┘
 99  
100  /-- If `f : α →ₛ β` is a simple function and `g : β → α →ₛ γ` is a family of simple functions,
101  then `f.bind g` binds the first argument of `g` to `f`. In other words, `f.bind g a = g (f a) a`. -/
102  def bind (f : α →ₛ β) (g : β → α →ₛ γ) : α →ₛ γ :=
id                  └┘            └┘      └┘ 
src                  └┘               └┘        └┘
typ                 └┘            └┘      └┘ 
doc                  └┘               └┘        └┘
103  ⟨λa, g (f a) a,
id            
typ           
104   λ c, is_measurable_cut (λa b, g b a ∈ ({c} : set γ)) f (λ b, (g b).measurable_sn c),
id        └───────────────┘               └─┘             └───────────┘  
src        └───────────────┘                     └─┘                  └───────────┘
typ       └───────────────┘               └─┘             └───────────┘  
105   finite_subset (finite_bUnion f.finite (λ b, (g b).finite)) $
id    └───────────┘  └───────────┘ └─────┘         └────┘
src   └───────────┘  └───────────┘  └─────┘            └────┘
typ   └───────────┘  └───────────┘ └─────┘         └────┘
106   by rintro _ ⟨a, rfl⟩; simp; exact ⟨_, ⟨a, rfl⟩, _, rfl⟩⟩
id                                                      └─┘
src      └───────────────┘  └──┘  └────┘ └─┘  └┘   └────┘└─┘
typ      └───────────────┘  └──┘  └────┘ └─┘ └┘   └────┘└─┘
doc      └───────────────┘  └──┘  └────┘ └─┘  └┘   └────┘   
txt      └───────────────┘  └──┘  └────┘ └─┘  └┘   └────┘   
par      └───────────────┘  └──┘  └────┘ └─┘  └┘   └────┘   
pid            └─────────┘              └─┘  └┘   └────┘   
st      └───────────────────────────────────────────────────┘
107  
108  @[simp] theorem bind_apply (f : α →ₛ β) (g : β → α →ₛ γ) (a) :
id                                    └┘            └┘ 
src                                    └┘               └┘
typ                                   └┘            └┘ 
doc    └──┘                            └┘               └┘
109    f.bind g a = g (f a) a := rfl
id     └───┘             └─┘
src     └───┘                   └─┘
typ    └───┘             └─┘
doc     └───┘
110  
111  /-- Restrict a simple function `f : α →ₛ β`` to a set `s`. If `s` is measurable,
112  then `f.restrict s a = if a ∈ s then f a else 0`, otherwise `f.restrict s = const α 0`. -/
113  def restrict [has_zero β] (f : α →ₛ β) (s : set α) : α →ₛ β :=
id                 └──────┘         └┘        └─┘      └┘ 
src                └──────┘           └┘         └─┘        └┘
typ                └──────┘         └┘        └─┘      └┘ 
doc                                   └┘                    └┘
114  if hs : is_measurable s then ite hs f (const α 0) else const α 0
id   └┘      └───────────┘       └─┘ └┘   └───┘          └───┘ 
src  └┘      └───────────┘        └─┘       └───┘           └───┘
typ  └┘      └───────────┘       └─┘ └┘   └───┘          └───┘ 
doc          └───────────┘                  └───┘           └───┘
115  
116  @[simp] theorem restrict_apply [has_zero β]
id                                   └──────┘ 
src                                  └──────┘
typ                                  └──────┘ 
doc    └──┘
117    (f : α →ₛ β) {s : set α} (hs : is_measurable s) (a) :
id           └┘        └─┘         └───────────┘ 
src           └┘         └─┘          └───────────┘
typ          └┘        └─┘         └───────────┘ 
doc           └┘                      └───────────┘
118    restrict f s a = if a ∈ s then f a else 0 :=
id     └──────┘                 
src    └──────┘             
typ    └──────┘                 
doc    └──────┘
119  by unfold_coes; simp [restrict, hs]; apply ite_apply hs
id                         └──────┘  └┘         └───────┘ └┘
src     └─────────┘  └────┘└──────┘└┘    └────┘└───────┘  
typ     └─────────┘  └────┘└──────┘└┘└┘  └────┘└───────┘└┘
doc     └─────────┘  └────┘└──────┘└┘    └────┘           
txt     └─────────┘  └────┘        └┘    └────┘           
par     └─────────┘  └────┘        └┘    └────┘           
pid                              └┘                    
st     └─────────────────────────────────────────────────────
120  
src  
typ  
doc  
txt  
par  
pid  
st   
121  theorem restrict_preimage [has_zero β]
id                              └──────┘ 
src                             └──────┘
typ                             └──────┘ 
122    (f : α →ₛ β) {s : set α} (hs : is_measurable s)
id           └┘        └─┘         └───────────┘ 
src           └┘         └─┘          └───────────┘
typ          └┘        └─┘         └───────────┘ 
doc           └┘                      └───────────┘
123    {t : set β} (ht : (0:β) ∉ t) : restrict f s ⁻¹' t = s ∩ f ⁻¹' t :=
id          └─┘                   └──────┘   └─┘      └─┘ 
src         └─┘                      └──────┘     └─┘         └─┘
typ         └─┘                   └──────┘   └─┘      └─┘ 
doc                                   └──────┘     └─┘           └─┘
124  by ext a; dsimp [preimage]; rw [restrict_apply]; by_cases a ∈ s; simp [h, hs, ht]
id                    └──────┘       └────────────┘                        └┘  └┘
src     └───┘  └─────┘└──────┘  └──┘└────────────┘  └───────┘    └────┘ └┘  └┘  └─
typ     └───┘  └─────┘└──────┘  └──┘└────────────┘  └───────┘  └────┘└┘└┘└┘└┘└─
doc     └───┘  └─────┘└──────┘  └──┘                └───────┘     └────┘ └┘  └┘  └─
txt     └───┘  └─────┘          └──┘                └───────┘     └────┘ └┘  └┘  └─
par     └───┘  └─────┘          └──┘                └───────┘     └────┘ └┘  └┘  └─
pid        └┘                   └┘                                  └┘  └┘  
st     └────────────────────────────┘└────────────┘└──────────────────────────────────
125  
src  
typ  
doc  
txt  
par  
pid  
st   
126  /-- Given a function `g : β → γ` and a simple function `f : α →ₛ β`, `f.map g` return the simple
127      function `g ∘ f : α →ₛ γ` -/
128  def map (g : β → γ) (f : α →ₛ β) : α →ₛ γ := bind f (const α ∘ g)
id                           └┘      └┘     └──┘   └───┘   
src                             └┘        └┘      └──┘    └───┘   
typ                          └┘      └┘     └──┘   └───┘   
doc                             └┘        └┘      └──┘    └───┘
129  
130  @[simp] theorem map_apply (g : β → γ) (f : α →ₛ β) (a) : f.map g a = g (f a) := rfl
id                                             └┘         └──┘            └─┘
src                                               └┘           └──┘                 └─┘
typ                                            └┘         └──┘            └─┘
doc    └──┘                                       └┘           └──┘
131  
132  theorem map_map (g : β → γ) (h: γ → δ) (f : α →ₛ β) : (f.map g).map h = f.map (h ∘ g) := rfl
id                                            └┘      └──┘  └─┘    └──┘         └─┘
src                                                └┘        └──┘   └─┘      └──┘           └─┘
typ                                           └┘      └──┘  └─┘    └──┘         └─┘
doc                                                └┘        └──┘   └─┘       └──┘
133  
134  theorem coe_map (g : β → γ) (f : α →ₛ β) : (f.map g : α → γ) = g ∘ f := rfl
id                                   └┘      └──┘                └─┘
src                                     └┘        └──┘                     └─┘
typ                                  └┘      └──┘                └─┘
doc                                     └┘        └──┘
135  
136  @[simp] theorem range_map [decidable_eq γ] (g : β → γ) (f : α →ₛ β) :
id                              └──────────┘                   └┘ 
src                             └──────────┘                       └┘
typ                             └──────────┘                   └┘ 
doc    └──┘                                                        └┘
137    (f.map g).range = f.range.image g :=
id      └──┘  └───┘   └────┘└────┘ 
src      └──┘   └───┘    └────┘└────┘
typ     └──┘  └───┘   └────┘└────┘ 
doc      └──┘   └───┘     └────┘└────┘
138  begin
st   └─────
139    ext c,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
140    simp only [mem_range, exists_prop, mem_range, finset.mem_image, map_apply],
id                └───────┘  └─────────┘  └───────┘  └──────────────┘  └───────┘
src    └─────────┘└───────┘└┘└─────────┘└┘└───────┘└┘└──────────────┘└┘└───────┘
typ    └─────────┘└───────┘└┘└─────────┘└┘└───────┘└┘└──────────────┘└┘└───────┘
doc    └─────────┘         └┘           └┘         └┘                └┘         
txt    └─────────┘         └┘           └┘         └┘                └┘         
par    └─────────┘         └┘           └┘         └┘                └┘         
pid        └──┘└┘         └┘           └┘         └┘                └┘         
st   ───────────────────────────────────────────────────────────────────────────┘└─
141    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
142    { rintros ⟨a, rfl⟩, exact ⟨f a, ⟨_, rfl⟩, rfl⟩ },
id                                             └─┘
src      └──────────────┘  └────┘   └┘ └─┘   └─┘└─┘└┘
typ      └──────────────┘  └────┘ └┘ └─┘   └─┘└─┘└┘
doc      └──────────────┘  └────┘   └┘ └─┘   └─┘   └┘
txt      └──────────────┘  └────┘   └┘ └─┘   └─┘   └┘
par      └──────────────┘  └────┘   └┘ └─┘   └─┘   └┘
pid             └───────┘          └┘ └─┘   └─┘   
st   ───┘└──────────────┘└───────────────────────────┘└┘
143    { rintros ⟨_, ⟨a, rfl⟩, rfl⟩, exact ⟨_, rfl⟩ }
id                                             └─┘
src      └────────────────────────┘  └────┘ └─┘└─┘└┘
typ      └────────────────────────┘  └────┘ └─┘└─┘└┘
doc      └────────────────────────┘  └────┘ └─┘   └┘
txt      └────────────────────────┘  └────┘ └─┘   └┘
par      └────────────────────────┘  └────┘ └─┘   └┘
pid             └─────────────────┘        └─┘   
st   ─────────────────────────────┘└───────────────┘└─
144  end
st   ──┘
145  
146  lemma map_preimage (f : α →ₛ β) (g : β → γ) (s : set γ) :
id                            └┘                  └─┘ 
src                            └┘                     └─┘
typ                           └┘                  └─┘ 
doc                            └┘
147    (f.map g) ⁻¹' s = (⋃b∈f.range.filter (λb, g b ∈ s), f ⁻¹' {b}) :=
id      └──┘   └─┘     └────┘└─────┘           └─┘ 
src      └──┘    └─┘        └────┘└─────┘                └─┘ 
typ     └──┘   └─┘     └────┘└─────┘           └─┘ 
doc      └──┘    └─┘         └────┘└─────┘                 └─┘
148  begin
st   └─────
149    /- True because `f` only takes finitely many values. -/
st   ──────────────────────────────────────────────────────────
150    ext a',
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid       └─┘
st   ───────┘└─
151    simp only [mem_Union, set.mem_preimage, exists_prop, set.mem_preimage, map_apply,
id                └───────┘  └──────────────┘  └─────────┘  └──────────────┘  └───────┘
src    └─────────┘└───────┘└┘└──────────────┘└┘└─────────┘└┘└──────────────┘└┘└───────┘└─
typ    └─────────┘└───────┘└┘└──────────────┘└┘└─────────┘└┘└──────────────┘└┘└───────┘└─
doc    └─────────┘         └┘                └┘           └┘                └┘         └─
txt    └─────────┘         └┘                └┘           └┘                └┘         └─
par    └─────────┘         └┘                └┘           └┘                └┘         └─
pid        └──┘└┘         └┘                └┘           └┘                └┘         └─
st   ────────────────────────────────────────────────────────────────────────────────────
152        finset.mem_filter, mem_range, mem_singleton_iff, exists_eq_right'],
id         └───────────────┘  └───────┘  └───────────────┘  └──────────────┘
src  ─────┘└───────────────┘└┘└───────┘└┘└───────────────┘└┘└──────────────┘
typ  ─────┘└───────────────┘└┘└───────┘└┘└───────────────┘└┘└──────────────┘
doc  ─────┘                 └┘         └┘                 └┘                
txt  ─────┘                 └┘         └┘                 └┘                
par  ─────┘                 └┘         └┘                 └┘                
pid  ─────┘                 └┘         └┘                 └┘                
st   ───────────────────────────────────────────────────────────────────────┘└─
153    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
154    { assume eq, exact ⟨⟨_, rfl⟩, eq⟩ },
id                             └─┘   └┘
src      └───────┘  └────┘  └─┘└─┘└─┘└┘└┘
typ      └───────┘  └────┘  └─┘└─┘└─┘└┘└┘
doc      └───────┘  └────┘  └─┘   └─┘  └┘
txt      └───────┘  └────┘  └─┘   └─┘  └┘
par      └───────┘  └────┘  └─┘   └─┘  └┘
pid      └───────┘         └─┘   └─┘  
st   ───┘└───────┘└─────────────────────┘└┘
155    { rintros ⟨_, eq⟩, exact eq }
id                              └┘
src      └─────────────┘  └────┘└┘
typ      └─────────────┘  └────┘└┘
doc      └─────────────┘  └────┘  
txt      └─────────────┘  └────┘  
par      └─────────────┘  └────┘  
pid             └──────┘         
st   ──────────────────┘└─────────┘└─
156  end
st   ──┘
157  
158  lemma map_preimage_singleton (f : α →ₛ β) (g : β → γ) (c : γ) :
id                                      └┘                  
src                                      └┘
typ                                     └┘                  
doc                                      └┘
159    (f.map g) ⁻¹' {c} = (⋃b∈f.range.filter (λb, g b = c), f ⁻¹' {b}) :=
id      └──┘   └─┘      └────┘└─────┘           └─┘ 
src      └──┘    └─┘         └────┘└─────┘                └─┘ 
typ     └──┘   └─┘      └────┘└─────┘           └─┘ 
doc      └──┘    └─┘           └────┘└─────┘                 └─┘
160  begin
st   └─────
161    rw map_preimage,
id        └──────────┘
src    └─┘└──────────┘
typ    └─┘└──────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────┘└─
162    have : (λb, g b = c) = λb, g b ∈ _root_.singleton c,
id                                   └──────────────┘ 
src    └─────┘  └─┘   └┘  └─┘  └──────────────┘
typ    └─────┘  └─┘   └┘  └─┘ └──────────────┘
doc    └─────┘  └─┘    └┘  └─┘                   
txt    └─────┘  └─┘    └┘  └─┘                   
par    └─────┘  └─┘    └┘  └─┘                   
pid    └───┘└┘  └─┘    └┘  └─┘                   
st   ────────────────────────────────────────────────────┘└─
163      funext, rw [eq_iff_iff, mem_singleton_iff],
id                   └────────┘  └───────────────┘
src      └────┘  └──┘└────────┘└┘└───────────────┘
typ      └────┘  └──┘└────────┘└┘└───────────────┘
doc      └────┘  └──┘          └┘                 
txt      └────┘  └──┘          └┘                 
par      └────┘  └──┘          └┘                 
pid                └┘          └┘                 
st   ─────────┘└──────────────┘└─────────────────┘└──
164    rw this
id        └──┘
src    └─┘    
typ    └─┘└──┘
doc    └─┘    
txt    └─┘    
par    └─┘    
pid          
st   ─────────┘
165  end
st   └─┘
166  
167  /-- If `f` is a simple function taking values in `β → γ` and `g` is another simple function
168  with the same domain and codomain `β`, then `f.seq g = f a (g a)`. -/
169  def seq (f : α →ₛ (β → γ)) (g : α →ₛ β) : α →ₛ γ := f.bind (λf, g.map f)
id                 └┘              └┘      └┘     └───┘     └──┘ 
src                 └┘                 └┘        └┘       └───┘       └──┘
typ                └┘              └┘      └┘     └───┘     └──┘ 
doc                 └┘                 └┘        └┘       └───┘       └──┘
170  
171  @[simp] lemma seq_apply (f : α →ₛ (β → γ)) (g : α →ₛ β) (a : α) : f.seq g a = f a (g a) := rfl
id                                 └┘              └┘            └──┘             └─┘
src                                 └┘                 └┘               └──┘                   └─┘
typ                                └┘              └┘            └──┘             └─┘
doc    └──┘                         └┘                 └┘               └──┘
172  
173  /-- Combine two simple functions `f : α →ₛ β` and `g : α →ₛ β`
174  into `λ a, (f a, g a)`. -/
175  def pair (f : α →ₛ β) (g : α →ₛ γ) : α →ₛ (β × γ) := (f.map prod.mk).seq g
id                  └┘         └┘      └┘          └──┘ └─────┘ └─┘  
src                  └┘           └┘        └┘             └──┘ └─────┘ └─┘
typ                 └┘         └┘      └┘          └──┘ └─────┘ └─┘  
doc                  └┘           └┘        └┘              └──┘         └─┘
176  
177  @[simp] lemma pair_apply (f : α →ₛ β) (g : α →ₛ γ) (a) : pair f g a = (f a, g a) := rfl
id                                  └┘         └┘         └──┘              └─┘
src                                  └┘           └┘          └──┘                     └─┘
typ                                 └┘         └┘         └──┘              └─┘
doc    └──┘                          └┘           └┘          └──┘
178  
179  lemma pair_preimage (f : α →ₛ β) (g : α →ₛ γ) (s : set β) (t : set γ) :
id                             └┘         └┘        └─┘        └─┘ 
src                             └┘           └┘         └─┘         └─┘
typ                            └┘         └┘        └─┘        └─┘ 
doc                             └┘           └┘
180    (pair f g) ⁻¹' (set.prod s t) = (f ⁻¹' s) ∩ (g ⁻¹' t) := rfl
id      └──┘    └─┘  └──────┘       └─┘      └─┘      └─┘
src     └──┘      └─┘  └──────┘          └─┘        └─┘       └─┘
typ     └──┘    └─┘  └──────┘       └─┘      └─┘      └─┘
doc     └──┘      └─┘  └──────┘           └─┘         └─┘
181  
182  /- A special form of `pair_preimage` -/
183  lemma pair_preimage_singleton (f : α →ₛ β) (g : α →ₛ γ) (b : β) (c : γ) :
id                                       └┘         └┘               
src                                       └┘           └┘
typ                                      └┘         └┘               
doc                                       └┘           └┘
184    (pair f g) ⁻¹' {(b, c)} = (f ⁻¹' {b}) ∩ (g ⁻¹' {c}) :=
id      └──┘    └─┘         └─┘       └─┘ 
src     └──┘      └─┘            └─┘         └─┘ 
typ     └──┘    └─┘         └─┘       └─┘ 
doc     └──┘      └─┘               └─┘           └─┘
185  by { rw ← prod_singleton_singleton, exact pair_preimage _ _ _ _ }
id             └──────────────────────┘        └───────────┘
src       └───┘└──────────────────────┘  └────┘└───────────┘└───────┘
typ       └───┘└──────────────────────┘  └────┘└───────────┘└───────┘
doc       └───┘                          └────┘             └───────┘
txt       └───┘                          └────┘             └───────┘
par       └───┘                          └────┘             └───────┘
pid         └─┘                                            └──────┘
st     └──────────────────────────────┘└────────────────────────────┘└┘
186  
187  theorem bind_const (f : α →ₛ β) : f.bind (const α) = f := by ext; simp
id                            └┘     └───┘  └───┘    
src                            └┘       └───┘  └───┘             └─┘  └────
typ                           └┘     └───┘  └───┘           └─┘  └────
doc                            └┘       └───┘  └───┘              └─┘  └────
txt                                                               └─┘  └────
par                                                               └─┘  └────
pid                                                                        
st                                                               └──────────
188  
src  
typ  
doc  
txt  
par  
pid  
st   
189  instance [has_zero β] : has_zero (α →ₛ β) := ⟨const α 0⟩
id             └──────┘     └──────┘   └┘       └───┘ 
src            └──────┘      └──────┘    └┘        └───┘
typ            └──────┘     └──────┘   └┘       └───┘ 
doc                                      └┘        └───┘
190  instance [has_add β] : has_add (α →ₛ β) := ⟨λf g, (f.map (+)).seq g⟩
id             └─────┘     └─────┘   └┘            └──┘    └─┘  
src            └─────┘      └─────┘    └┘                └──┘    └─┘
typ            └─────┘     └─────┘   └┘            └──┘    └─┘  
doc                                    └┘                └──┘     └─┘
191  instance [has_mul β] : has_mul (α →ₛ β) := ⟨λf g, (f.map (*)).seq g⟩
id             └─────┘     └─────┘   └┘            └──┘    └─┘  
src            └─────┘      └─────┘    └┘                └──┘    └─┘
typ            └─────┘     └─────┘   └┘            └──┘    └─┘  
doc                                    └┘                └──┘     └─┘
192  instance [has_sup β] : has_sup (α →ₛ β) := ⟨λf g, (f.map (⊔)).seq g⟩
id             └─────┘     └─────┘   └┘            └──┘    └─┘  
src            └─────┘      └─────┘    └┘                └──┘    └─┘
typ            └─────┘     └─────┘   └┘            └──┘    └─┘  
doc            └─────┘      └─────┘    └┘                └──┘     └─┘
193  instance [has_inf β] : has_inf (α →ₛ β) := ⟨λf g, (f.map (⊓)).seq g⟩
id             └─────┘     └─────┘   └┘            └──┘    └─┘  
src            └─────┘      └─────┘    └┘                └──┘    └─┘
typ            └─────┘     └─────┘   └┘            └──┘    └─┘  
doc            └─────┘      └─────┘    └┘                └──┘     └─┘
194  instance [has_le β] : has_le (α →ₛ β) := ⟨λf g, ∀a, f a ≤ g a⟩
id             └────┘     └────┘   └┘                  
src            └────┘      └────┘    └┘                      
typ            └────┘     └────┘   └┘                  
doc                                  └┘
195  
196  @[simp] lemma sup_apply [has_sup β] (f g : α →ₛ β) (a : α) : (f ⊔ g) a = f a ⊔ g a := rfl
id                            └─────┘           └┘                           └─┘
src                           └─────┘             └┘                                    └─┘
typ                           └─────┘           └┘                           └─┘
doc    └──┘                   └─────┘             └┘
197  @[simp] lemma mul_apply [has_mul β] (f g : α →ₛ β) (a : α) : (f * g) a = f a * g a := rfl
id                            └─────┘           └┘                           └─┘
src                           └─────┘             └┘                                    └─┘
typ                           └─────┘           └┘                           └─┘
doc    └──┘                                       └┘
198  lemma add_apply [has_add β] (f g : α →ₛ β) (a : α) : (f + g) a = f a + g a := rfl
id                    └─────┘           └┘                           └─┘
src                   └─────┘             └┘                                    └─┘
typ                   └─────┘           └┘                           └─┘
doc                                       └┘
199  
200  lemma add_eq_map₂ [has_add β] (f g : α →ₛ β) : f + g = (pair f g).map (λp:β×β, p.1 + p.2) :=
id                      └─────┘           └┘          └──┘   └─┘           
src                     └─────┘             └┘             └──┘     └─┘               
typ                     └─────┘           └┘          └──┘   └─┘           
doc                                         └┘               └──┘     └─┘
201  rfl
id   └─┘
src  └─┘
typ  └─┘
202  
203  lemma sup_eq_map₂ [has_sup β] (f g : α →ₛ β) : f ⊔ g = (pair f g).map (λp:β×β, p.1 ⊔ p.2) :=
id                      └─────┘           └┘          └──┘   └─┘           
src                     └─────┘             └┘             └──┘     └─┘               
typ                     └─────┘           └┘          └──┘   └─┘           
doc                     └─────┘             └┘               └──┘     └─┘
204  rfl
id   └─┘
src  └─┘
typ  └─┘
205  
206  lemma const_mul_eq_map [has_mul β] (f : α →ₛ β) (b : β) : const α b * f = f.map (λa, b * a) := rfl
id                           └─────┘         └┘            └───┘      └──┘            └─┘
src                          └─────┘           └┘              └───┘          └──┘               └─┘
typ                          └─────┘         └┘            └───┘      └──┘            └─┘
doc                                            └┘              └───┘            └──┘
207  
208  instance [add_monoid β] : add_monoid (α →ₛ β) :=
id             └────────┘     └────────┘   └┘ 
src            └────────┘      └────────┘    └┘
typ            └────────┘     └────────┘   └┘ 
doc                                          └┘
209  { add       := (+), zero := 0,
id                  
src                 
typ                 
210    add_assoc := assume f g h, ext (assume a, add_assoc _ _ _),
id                             └─┘           └───────┘
src                               └─┘            └───────┘
typ                            └─┘           └───────┘
211    zero_add  := assume f, ext (assume a, zero_add _),
id                           └─┘           └──────┘
src                           └─┘            └──────┘
typ                          └─┘           └──────┘
212    add_zero  := assume f, ext (assume a, add_zero _) }
id                           └─┘           └──────┘
src                           └─┘            └──────┘
typ                          └─┘           └──────┘
213  
214  instance add_comm_monoid [add_comm_monoid β] : add_comm_monoid (α →ₛ β) :=
id                             └─────────────┘     └─────────────┘   └┘ 
src                            └─────────────┘      └─────────────┘    └┘
typ                            └─────────────┘     └─────────────┘   └┘ 
doc                                                                    └┘
215  { add_comm := λ f g, ext (λa, add_comm _ _),
id                      └─┘     └──────┘
src                       └─┘      └──────┘
typ                     └─┘     └──────┘
216    .. simple_func.add_monoid }
id        └────────────────────┘
src       └────────────────────┘
typ       └────────────────────┘
217  
218  instance [has_neg β] : has_neg (α →ₛ β) := ⟨λf, f.map (has_neg.neg)⟩
id             └─────┘     └─────┘   └┘          └──┘  └─────────┘
src            └─────┘      └─────┘    └┘             └──┘  └─────────┘
typ            └─────┘     └─────┘   └┘          └──┘  └─────────┘
doc                                    └┘             └──┘
219  
220  instance [add_group β] : add_group (α →ₛ β) :=
id             └───────┘     └───────┘   └┘ 
src            └───────┘      └───────┘    └┘
typ            └───────┘     └───────┘   └┘ 
doc                                        └┘
221  { neg := has_neg.neg,
id            └─────────┘
src           └─────────┘
typ           └─────────┘
222    add_left_neg := λf, ext (λa, add_left_neg _),
id                        └─┘     └──────────┘
src                        └─┘      └──────────┘
typ                       └─┘     └──────────┘
223    .. simple_func.add_monoid }
id        └────────────────────┘
src       └────────────────────┘
typ       └────────────────────┘
224  
225  instance [add_comm_group β] : add_comm_group (α →ₛ β) :=
id             └────────────┘     └────────────┘   └┘ 
src            └────────────┘      └────────────┘    └┘
typ            └────────────┘     └────────────┘   └┘ 
doc                                                  └┘
226  { add_comm := λ f g, ext (λa, add_comm _ _) ,
id                      └─┘     └──────┘
src                       └─┘      └──────┘
typ                     └─┘     └──────┘
227    .. simple_func.add_group }
id        └───────────────────┘
src       └───────────────────┘
typ       └───────────────────┘
228  
229  variables {K : Type*}
230  
231  instance [has_scalar K β] : has_scalar K (α →ₛ β) := ⟨λk f, f.map (λb, k • b)⟩
id             └────────┘      └────────┘    └┘           └──┘       
src            └────────┘        └────────┘      └┘               └──┘        
typ            └────────┘      └────────┘    └┘           └──┘       
doc            └────────┘        └────────┘      └┘               └──┘
232  
233  instance [semiring K] [add_comm_monoid β] [semimodule K β] : semimodule K (α →ₛ β) :=
id             └──────┘    └─────────────┘    └────────┘      └────────┘    └┘ 
src            └──────┘     └─────────────┘     └────────┘        └────────┘      └┘
typ            └──────┘    └─────────────┘    └────────┘      └────────┘    └┘ 
doc                                             └────────┘        └────────┘      └┘
234  { one_smul := λ f, ext (λa, one_smul _ _),
id                     └─┘     └──────┘
src                     └─┘      └──────┘
typ                    └─┘     └──────┘
235    mul_smul := λ x y f, ext (λa, mul_smul _ _ _),
id                       └─┘     └──────┘
src                         └─┘      └──────┘
typ                      └─┘     └──────┘
236    smul_add := λ r f g, ext (λa, smul_add _ _ _),
id                       └─┘     └──────┘
src                         └─┘      └──────┘
typ                      └─┘     └──────┘
237    smul_zero := λ r, ext (λa, smul_zero _),
id                      └─┘     └───────┘
src                      └─┘      └───────┘
typ                     └─┘     └───────┘
238    add_smul := λ r s f, ext (λa, add_smul _ _ _),
id                       └─┘     └──────┘
src                         └─┘      └──────┘
typ                      └─┘     └──────┘
239    zero_smul := λ f, ext (λa, zero_smul _ _) }
id                      └─┘     └───────┘
src                      └─┘      └───────┘
typ                     └─┘     └───────┘
240  
241  instance [ring K] [add_comm_group β] [module K β] : module K (α →ₛ β) :=
id             └──┘    └────────────┘    └────┘      └────┘    └┘ 
src            └──┘     └────────────┘     └────┘        └────┘      └┘
typ            └──┘    └────────────┘    └────┘      └────┘    └┘ 
doc                                        └────┘        └────┘      └┘
242  { .. simple_func.semimodule }
id        └────────────────────┘
src       └────────────────────┘
typ       └────────────────────┘
243  
244  instance [discrete_field K] [add_comm_group β] [module K β] : vector_space K (α →ₛ β) :=
id             └────────────┘    └────────────┘    └────┘      └──────────┘    └┘ 
src            └────────────┘     └────────────┘     └────┘        └──────────┘      └┘
typ            └────────────┘    └────────────┘    └────┘      └──────────┘    └┘ 
doc                                                  └────┘        └──────────┘      └┘
245  { .. simple_func.module }
id        └────────────────┘
src       └────────────────┘
typ       └────────────────┘
246  
247  lemma smul_apply [has_scalar K β] (k : K) (f : α →ₛ β) (a : α) : (k • f) a = k • f a := rfl
id                     └────────┘                 └┘                          └─┘
src                    └────────┘                     └┘                                  └─┘
typ                    └────────┘                 └┘                          └─┘
doc                    └────────┘                     └┘
248  
249  lemma smul_eq_map [has_scalar K β] (k : K) (f : α →ₛ β) : k • f = f.map (λb, k • b) := rfl
id                      └────────┘                 └┘         └──┘            └─┘
src                     └────────┘                     └┘             └──┘               └─┘
typ                     └────────┘                 └┘         └──┘            └─┘
doc                     └────────┘                     └┘               └──┘
250  
251  instance [preorder β] : preorder (α →ₛ β) :=
id             └──────┘     └──────┘   └┘ 
src            └──────┘      └──────┘    └┘
typ            └──────┘     └──────┘   └┘ 
doc                                      └┘
252  { le_refl := λf a, le_refl _,
id                   └─────┘
src                    └─────┘
typ                  └─────┘
253    le_trans := λf g h hfg hgh a, le_trans (hfg _) (hgh a),
id                     └─┘ └─┘   └──────┘  └─┘     └─┘ 
src                                  └──────┘
typ                    └─┘ └─┘   └──────┘  └─┘     └─┘ 
254    .. simple_func.has_le }
id        └────────────────┘
src       └────────────────┘
typ       └────────────────┘
255  
256  instance [partial_order β] : partial_order (α →ₛ β) :=
id             └───────────┘     └───────────┘   └┘ 
src            └───────────┘      └───────────┘    └┘
typ            └───────────┘     └───────────┘   └┘ 
doc                                                └┘
257  { le_antisymm := assume f g hfg hgf, ext $ assume a, le_antisymm (hfg a) (hgf a),
id                             └─┘ └─┘  └─┘            └─────────┘  └─┘    └─┘ 
src                                       └─┘             └─────────┘
typ                            └─┘ └─┘  └─┘            └─────────┘  └─┘    └─┘ 
258    .. simple_func.preorder }
id        └──────────────────┘
src       └──────────────────┘
typ       └──────────────────┘
259  
260  instance [order_bot β] : order_bot (α →ₛ β) :=
id             └───────┘     └───────┘   └┘ 
src            └───────┘      └───────┘    └┘
typ            └───────┘     └───────┘   └┘ 
doc            └───────┘      └───────┘    └┘
261  { bot := const α ⊥, bot_le := λf a, bot_le, .. simple_func.partial_order }
id            └───┘                  └────┘     └───────────────────────┘
src           └───┘                     └────┘     └───────────────────────┘
typ           └───┘                  └────┘     └───────────────────────┘
doc           └───┘
262  
263  instance [order_top β] : order_top (α →ₛ β) :=
id             └───────┘     └───────┘   └┘ 
src            └───────┘      └───────┘    └┘
typ            └───────┘     └───────┘   └┘ 
doc            └───────┘      └───────┘    └┘
264  { top := const α⊤, le_top := λf a, le_top, .. simple_func.partial_order }
id            └───┘                 └────┘     └───────────────────────┘
src           └───┘                    └────┘     └───────────────────────┘
typ           └───┘                 └────┘     └───────────────────────┘
doc           └───┘
265  
266  instance [semilattice_inf β] : semilattice_inf (α →ₛ β) :=
id             └─────────────┘     └─────────────┘   └┘ 
src            └─────────────┘      └─────────────┘    └┘
typ            └─────────────┘     └─────────────┘   └┘ 
doc            └─────────────┘      └─────────────┘    └┘
267  { inf := (⊓),
id            
src           
typ           
268    inf_le_left := assume f g a, inf_le_left,
id                               └─────────┘
src                                 └─────────┘
typ                              └─────────┘
269    inf_le_right := assume f g a, inf_le_right,
id                                └──────────┘
src                                  └──────────┘
typ                               └──────────┘
270    le_inf := assume f g h hfh hgh a, le_inf (hfh a) (hgh a),
id                         └─┘ └─┘   └────┘  └─┘    └─┘ 
src                                      └────┘
typ                        └─┘ └─┘   └────┘  └─┘    └─┘ 
271    .. simple_func.partial_order }
id        └───────────────────────┘
src       └───────────────────────┘
typ       └───────────────────────┘
272  
273  instance [semilattice_sup β] : semilattice_sup (α →ₛ β) :=
id             └─────────────┘     └─────────────┘   └┘ 
src            └─────────────┘      └─────────────┘    └┘
typ            └─────────────┘     └─────────────┘   └┘ 
doc            └─────────────┘      └─────────────┘    └┘
274  { sup := (⊔),
id            
src           
typ           
275    le_sup_left := assume f g a, le_sup_left,
id                               └─────────┘
src                                 └─────────┘
typ                              └─────────┘
276    le_sup_right := assume f g a, le_sup_right,
id                                └──────────┘
src                                  └──────────┘
typ                               └──────────┘
277    sup_le := assume f g h hfh hgh a, sup_le (hfh a) (hgh a),
id                         └─┘ └─┘   └────┘  └─┘    └─┘ 
src                                      └────┘
typ                        └─┘ └─┘   └────┘  └─┘    └─┘ 
278    .. simple_func.partial_order }
id        └───────────────────────┘
src       └───────────────────────┘
typ       └───────────────────────┘
279  
280  instance [semilattice_sup_bot β] : semilattice_sup_bot (α →ₛ β) :=
id             └─────────────────┘     └─────────────────┘   └┘ 
src            └─────────────────┘      └─────────────────┘    └┘
typ            └─────────────────┘     └─────────────────┘   └┘ 
doc            └─────────────────┘      └─────────────────┘    └┘
281  { .. simple_func.lattice.semilattice_sup,.. simple_func.lattice.order_bot }
id        └─────────────────────────────────┘    └───────────────────────────┘
src       └─────────────────────────────────┘    └───────────────────────────┘
typ       └─────────────────────────────────┘    └───────────────────────────┘
282  
283  instance [lattice β] : lattice (α →ₛ β) :=
id             └─────┘     └─────┘   └┘ 
src            └─────┘      └─────┘    └┘
typ            └─────┘     └─────┘   └┘ 
doc            └─────┘      └─────┘    └┘
284  { .. simple_func.lattice.semilattice_sup,.. simple_func.lattice.semilattice_inf }
id        └─────────────────────────────────┘    └─────────────────────────────────┘
src       └─────────────────────────────────┘    └─────────────────────────────────┘
typ       └─────────────────────────────────┘    └─────────────────────────────────┘
285  
286  instance [bounded_lattice β] : bounded_lattice (α →ₛ β) :=
id             └─────────────┘     └─────────────┘   └┘ 
src            └─────────────┘      └─────────────┘    └┘
typ            └─────────────┘     └─────────────┘   └┘ 
doc            └─────────────┘      └─────────────┘    └┘
287  { .. simple_func.lattice.lattice, .. simple_func.lattice.order_bot, .. simple_func.lattice.order_top }
id        └─────────────────────────┘     └───────────────────────────┘     └───────────────────────────┘
src       └─────────────────────────┘     └───────────────────────────┘     └───────────────────────────┘
typ       └─────────────────────────┘     └───────────────────────────┘     └───────────────────────────┘
288  
289  lemma finset_sup_apply [semilattice_sup_bot β] {f : γ → α →ₛ β} (s : finset γ) (a : α) :
id                           └─────────────────┘            └┘        └────┘        
src                          └─────────────────┘               └┘         └────┘
typ                          └─────────────────┘            └┘        └────┘        
doc                          └─────────────────┘               └┘         └────┘
290    s.sup f a = s.sup (λc, f c a) :=
id     └──┘    └──┘       
src     └──┘       └──┘
typ    └──┘    └──┘       
doc     └──┘        └──┘
291  begin
st   └─────
292    refine finset.induction_on s rfl _,
id            └─────────────────┘  └─┘
src    └─────┘└─────────────────┘ └─┘└┘
typ    └─────┘└─────────────────┘└─┘└┘
doc    └─────┘└─────────────────┘    └┘
txt    └─────┘                       └┘
par    └─────┘                       └┘
pid                                 └┘
st   ───────────────────────────────────┘└─
293    assume a s hs ih,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid    └──────────────┘
st   ─────────────────┘└─
294    rw [finset.sup_insert, finset.sup_insert, sup_apply, ih]
id         └───────────────┘  └───────────────┘  └───────┘  └┘
src    └──┘└───────────────┘└┘└───────────────┘└┘└───────┘└┘  └┘
typ    └──┘└───────────────┘└┘└───────────────┘└┘└───────┘└┘└┘└┘
doc    └──┘                 └┘                 └┘         └┘  └┘
txt    └──┘                 └┘                 └┘         └┘  └┘
par    └──┘                 └┘                 └┘         └┘  └┘
pid      └┘                 └┘                 └┘         └┘  
st   ──────────────────────┘└─────────────────┘└─────────┘└──┘
295  end
st   └─┘
296  
297  section approx
298  
299  section
300  variables [semilattice_sup_bot β] [has_zero β]
id              └─────────────────┘     └──────┘
src             └─────────────────┘     └──────┘
typ             └─────────────────┘     └──────┘
doc             └─────────────────┘
301  
302  /-- Fix a sequence `i : ℕ → β`. Given a function `α → β`, its `n`-th approximation
303  by simple functions is defined so that in case `β = ennreal` it sends each `a` to the supremum
304  of the set `{i k | k ≤ n ∧ i k ≤ f a}`, see `approx_apply` and `supr_approx_apply` for details. -/
305  def approx (i : ℕ → β) (f : α → β) (n : ℕ) : α →ₛ β :=
id                                            └┘ 
src                                               └┘
typ                                           └┘ 
doc                                                 └┘
306  (finset.range n).sup (λk, restrict (const α (i k)) {a:α | i k ≤ f a})
id    └──────────┘  └─┘      └──────┘  └───┘                
src   └──────────┘   └─┘       └──────┘  └───┘                    
typ   └──────────┘  └─┘      └──────┘  └───┘                
doc   └──────────┘   └─┘       └──────┘  └───┘
307  
308  lemma approx_apply [topological_space β] [order_closed_topology β] {i : ℕ → β} {f : α → β} {n : ℕ}
id                       └───────────────┘    └───────────────────┘                            
src                      └───────────────┘     └───────────────────┘                                
typ                      └───────────────┘    └───────────────────┘                            
doc                      └───────────────┘     └───────────────────┘
309    (a : α) (hf : _root_.measurable f) :
id                  └───────────────┘ 
src                  └───────────────┘
typ                 └───────────────┘ 
doc                  └───────────────┘
310    (approx i f n : α →ₛ β) a = (finset.range n).sup (λk, if i k ≤ f a then i k else 0) :=
id      └────┘       └┘      └──────────┘  └─┘                    
src     └────┘           └┘        └──────────┘   └─┘              
typ     └────┘       └┘      └──────────┘  └─┘                    
doc     └────┘           └┘         └──────────┘   └─┘
311  begin
st   └─────
312    dsimp only [approx],
id                 └────┘
src    └──────────┘└────┘
typ    └──────────┘└────┘
doc    └──────────┘└────┘
txt    └──────────┘      
par    └──────────┘      
pid         └───┘└┘      
st   ────────────────────┘└─
313    rw [finset_sup_apply],
id         └──────────────┘
src    └──┘└──────────────┘
typ    └──┘└──────────────┘
doc    └──┘                
txt    └──┘                
par    └──┘                
pid      └┘                
st   ─────────────────────┘└──
314    congr,
src    └───┘
typ    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
315    funext k,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          └┘
st   ─────────┘└─
316    rw [restrict_apply],
id         └────────────┘
src    └──┘└────────────┘
typ    └──┘└────────────┘
doc    └──┘              
txt    └──┘              
par    └──┘              
pid      └┘              
st   ───────────────────┘└──
317    refl,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
318    exact (hf.preimage $ is_measurable_of_is_closed $ is_closed_ge' _)
id            └─────────┘   └────────────────────────┘   └───────────┘
src    └────┘ └─────────┘ └────────────────────────┘ └───────────┘└──┘
typ    └────┘ └─────────┘ └────────────────────────┘ └───────────┘└──┘
doc    └────┘                                                     └──┘
txt    └────┘                                                     └──┘
par    └────┘                                                     └──┘
pid                                                              └─┘
st   ────────────────────────────────────────────────────────────────────┘
319  end
st   └─┘
320  
321  lemma monotone_approx (i : ℕ → β) (f : α → β) : monotone (approx i f) :=
id                                               └──────┘  └────┘  
src                                                 └──────┘  └────┘
typ                                              └──────┘  └────┘  
doc                                                  └──────┘  └────┘
322  assume n m h, finset.sup_mono $ finset.range_subset.2 h
id              └─────────────┘   └─────────────────┘  
src                └─────────────┘   └─────────────────┘
typ             └─────────────┘   └─────────────────┘  
323  
324  lemma approx_comp [topological_space β] [order_closed_topology β] [measurable_space γ]
id                      └───────────────┘    └───────────────────┘    └──────────────┘ 
src                     └───────────────┘     └───────────────────┘     └──────────────┘
typ                     └───────────────┘    └───────────────────┘    └──────────────┘ 
doc                     └───────────────┘     └───────────────────┘
325    {i : ℕ → β} {f : γ → β} {g : α → γ} {n : ℕ} (a : α)
id                                               
src                                            
typ                                              
326    (hf : _root_.measurable f) (hg : _root_.measurable g) :
id           └───────────────┘         └───────────────┘ 
src          └───────────────┘          └───────────────┘
typ          └───────────────┘         └───────────────┘ 
doc          └───────────────┘          └───────────────┘
327    (approx i (f ∘ g) n : α →ₛ β) a = (approx i f n : γ →ₛ β) (g a) :=
id      └────┘           └┘      └────┘       └┘     
src     └────┘                └┘        └────┘           └┘
typ     └────┘           └┘      └────┘       └┘     
doc     └────┘                 └┘         └────┘           └┘
328  by rw [approx_apply _ hf, approx_apply _ (hf.comp hg)]
id          └──────────┘   └┘  └──────────┘    └─────┘ └┘
src     └──┘└──────────┘└─┘  └┘└──────────┘└─┘ └─────┘  └──
typ     └──┘└──────────┘└─┘└┘└┘└──────────┘└─┘ └─────┘└┘└──
doc     └──┘            └─┘  └┘            └─┘          └──
txt     └──┘            └─┘  └┘            └─┘          └──
par     └──┘            └─┘  └┘            └─┘          └──
pid       └┘            └─┘  └┘            └─┘          └┘
st     └────────────────────┘└───────────────────────────┘
329  
src  
typ  
doc  
txt  
par  
pid  
st   
330  end
331  
332  lemma supr_approx_apply [topological_space β] [complete_lattice β] [order_closed_topology β] [has_zero β]
id                            └───────────────┘    └──────────────┘    └───────────────────┘    └──────┘ 
src                           └───────────────┘     └──────────────┘     └───────────────────┘     └──────┘
typ                           └───────────────┘    └──────────────┘    └───────────────────┘    └──────┘ 
doc                           └───────────────┘     └──────────────┘     └───────────────────┘
333    (i : ℕ → β) (f : α → β) (a : α) (hf : _root_.measurable f) (h_zero : (0 : β) = ⊥) :
id                                      └───────────────┘                     
src                                         └───────────────┘                       
typ                                     └───────────────┘                     
doc                                          └───────────────┘
334    (⨆n, (approx i f n : α →ₛ β) a) = (⨆k (h : i k ≤ f a), i k) :=
id        └────┘       └┘                    
src        └────┘           └┘                         
typ       └────┘       └┘                    
doc        └────┘           └┘                           
335  begin
st   └─────
336    refine le_antisymm (supr_le $ assume n, _) (supr_le $ assume k, supr_le $ assume hk, _),
id            └─────────┘                                              └─────┘
src    └─────┘└─────────┘               └─────┘               └──┘└─────┘       └─────┘
typ    └─────┘└─────────┘               └─────┘               └──┘└─────┘       └─────┘
doc    └─────┘                          └─────┘               └──┘              └─────┘
txt    └─────┘                          └─────┘               └──┘              └─────┘
par    └─────┘                          └─────┘               └──┘              └─────┘
pid                                    └─────┘               └──┘              └─────┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
337    { rw [approx_apply a hf, h_zero],
id           └──────────┘  └┘  └────┘
src      └──┘└──────────┘   └┘      
typ      └──┘└──────────┘└┘└┘└────┘
doc      └──┘               └┘      
txt      └──┘               └┘      
par      └──┘               └┘      
pid        └┘               └┘      
st   ───┘└───────────────────┘└──────┘└──
338      refine finset.sup_le (assume k hk, _),
id              └───────────┘
src      └─────┘└───────────┘       └───────┘
typ      └─────┘└───────────┘       └───────┘
doc      └─────┘                    └───────┘
txt      └─────┘                    └───────┘
par      └─────┘                    └───────┘
pid                                └───────┘
st   ────────────────────────────────────────┘└─
339      split_ifs,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
st   ────────────┘└─
340      exact le_supr_of_le k (le_supr _ h),
id             └───────────┘   └─────┘   
src      └────┘└───────────┘  └─────┘└─┘ 
typ      └────┘└───────────┘ └─────┘└─┘
doc      └────┘                      └─┘ 
txt      └────┘                      └─┘ 
par      └────┘                      └─┘ 
pid                                 └─┘ 
st   ──────────────────────────────────────┘└─
341      exact bot_le },
id             └────┘
src      └────┘└────┘
typ      └────┘└────┘
doc      └────┘      
txt      └────┘      
par      └────┘      
pid                 
st   ────────────────┘└┘
342    { refine le_supr_of_le (k+1) _,
id              └───────────┘  
src      └─────┘└───────────┘  └──┘
typ      └─────┘└───────────┘ └──┘
doc      └─────┘                └──┘
txt      └─────┘                └──┘
par      └─────┘                └──┘
pid                            └──┘
st   ───────────────────────────────┘└─
343      rw [approx_apply a hf],
id           └──────────┘  └┘
src      └──┘└──────────┘   
typ      └──┘└──────────┘└┘
doc      └──┘               
txt      └──┘               
par      └──┘               
pid        └┘               
st   ────────────────────────┘└──
344      have : k ∈ finset.range (k+1) := finset.mem_range.2 (nat.lt_succ_self _),
id                 └──────────┘         └──────────────┘    └──────────────┘
src      └─────┘ └──────────┘   └────┘└──────────────┘└─┘ └──────────────┘└─┘
typ      └─────┘ └──────────┘  └────┘└──────────────┘└─┘ └──────────────┘└─┘
doc      └─────┘  └──────────┘   └────┘                └─┘                 └─┘
txt      └─────┘                 └────┘                └─┘                 └─┘
par      └─────┘                 └────┘                └─┘                 └─┘
pid      └───┘└┘                 └┘└──┘                └─┘                 └─┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
345      refine le_trans (le_of_eq _) (finset.le_sup this),
id              └──────┘  └──────┘     └───────────┘ └──┘
src      └─────┘└──────┘ └──────┘└──┘ └───────────┘    
typ      └─────┘└──────┘ └──────┘└──┘ └───────────┘└──┘
doc      └─────┘                 └──┘                  
txt      └─────┘                 └──┘                  
par      └─────┘                 └──┘                  
pid                             └──┘                  
st   ────────────────────────────────────────────────────┘└─
346      rw [if_pos hk] }
id           └────┘ └┘
src      └──┘└────┘  └┘
typ      └──┘└────┘└┘└┘
doc      └──┘        └┘
txt      └──┘        └┘
par      └──┘        └┘
pid        └┘        
st   ────────────────┘└─
347  end
st   ──┘
348  
349  end approx
350  
351  section eapprox
352  
353  /-- A sequence of `ennreal`s such that its range is the set of non-negative rational numbers. -/
354  def ennreal_rat_embed (n : ℕ) : ennreal :=
id                                  └─────┘
src                                 └─────┘
typ                                 └─────┘
doc                                  └─────┘
355  nnreal.of_real ((encodable.decode ℚ n).get_or_else (0 : ℚ))
id   └────────────┘   └──────────────┘   └─────────┘       
src  └────────────┘   └──────────────┘    └─────────┘       
typ  └────────────┘   └──────────────┘   └─────────┘       
doc                                                         
356  
357  lemma ennreal_rat_embed_encode (q : ℚ) :
id                                       
src                                      
typ                                      
doc                                      
358    ennreal_rat_embed (encodable.encode q) = nnreal.of_real q :=
id     └───────────────┘  └──────────────┘    └────────────┘ 
src    └───────────────┘  └──────────────┘     └────────────┘
typ    └───────────────┘  └──────────────┘    └────────────┘ 
doc    └───────────────┘
359  by rw [ennreal_rat_embed, encodable.encodek]; refl
id          └───────────────┘  └───────────────┘
src     └──┘└───────────────┘└┘└───────────────┘  └────
typ     └──┘└───────────────┘└┘└───────────────┘  └────
doc     └──┘└───────────────┘└┘                   └────
txt     └──┘                 └┘                   └────
par     └──┘                 └┘                   └────
pid       └┘                 └┘                       
st     └────────────────────┘└─────────────────┘└──────
360  
src  
typ  
doc  
txt  
par  
pid  
st   
361  def eapprox : (α → ennreal) → ℕ → α →ₛ ennreal :=
id                    └─────┘        └┘ └─────┘
src                     └─────┘         └┘ └─────┘
typ                   └─────┘        └┘ └─────┘
doc                     └─────┘          └┘ └─────┘
362  approx ennreal_rat_embed
id   └────┘ └───────────────┘
src  └────┘ └───────────────┘
typ  └────┘ └───────────────┘
doc  └────┘ └───────────────┘
363  
364  lemma monotone_eapprox (f : α → ennreal) : monotone (eapprox f) :=
id                                  └─────┘    └──────┘  └─────┘ 
src                                  └─────┘    └──────┘  └─────┘
typ                                 └─────┘    └──────┘  └─────┘ 
doc                                  └─────┘    └──────┘
365  monotone_approx _ f
id   └─────────────┘   
src  └─────────────┘
typ  └─────────────┘   
366  
367  lemma supr_eapprox_apply (f : α → ennreal) (hf : _root_.measurable f) (a : α) :
id                                    └─────┘        └───────────────┘        
src                                    └─────┘        └───────────────┘
typ                                   └─────┘        └───────────────┘        
doc                                    └─────┘        └───────────────┘
368    (⨆n, (eapprox f n : α →ₛ ennreal) a) = f a :=
id        └─────┘      └┘ └─────┘      
src        └─────┘         └┘ └─────┘     
typ       └─────┘      └┘ └─────┘      
doc                        └┘ └─────┘
369  begin
st   └─────
370    rw [eapprox, supr_approx_apply ennreal_rat_embed f a hf rfl],
id         └─────┘  └───────────────┘ └───────────────┘   └┘ └─┘
src    └──┘└─────┘└┘└───────────────┘└───────────────┘    └─┘
typ    └──┘└─────┘└┘└───────────────┘└───────────────┘└┘└─┘
doc    └──┘       └┘                 └───────────────┘       
txt    └──┘       └┘                                         
par    └──┘       └┘                                         
pid      └┘       └┘                                         
st   ────────────┘└──────────────────────────────────────────────┘└──
371    refine le_antisymm (supr_le $ assume i, supr_le $ assume hi, hi) (le_of_not_gt _),
id            └─────────┘                      └─────┘                   └──────────┘
src    └─────┘└─────────┘               └──┘└─────┘       └───┘  └┘ └──────────┘└─┘
typ    └─────┘└─────────┘               └──┘└─────┘       └───┘  └┘ └──────────┘└─┘
doc    └─────┘                          └──┘              └───┘  └┘             └─┘
txt    └─────┘                          └──┘              └───┘  └┘             └─┘
par    └─────┘                          └──┘              └───┘  └┘             └─┘
pid                                    └──┘              └───┘  └┘             └─┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
372    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
373    rcases ennreal.lt_iff_exists_rat_btwn.1 h with ⟨q, hq, lt_q, q_lt⟩,
id            └────────────────────────────┘   
src    └─────┘└────────────────────────────┘└─┘ └───────────────────────┘
typ    └─────┘└────────────────────────────┘└─┘└───────────────────────┘
doc    └─────┘                              └─┘ └───────────────────────┘
txt    └─────┘                              └─┘ └───────────────────────┘
par    └─────┘                              └─┘ └───────────────────────┘
pid                                        └─┘ └───────────────────────┘
st   ───────────────────────────────────────────────────────────────────┘└─
374    have : (nnreal.of_real q : ennreal) ≤
id             └────────────┘    └─────┘  
src    └─────┘ └────────────┘ └─┘└─────┘└┘
typ    └─────┘ └────────────┘└─┘└─────┘└┘
doc    └─────┘                └─┘└─────┘└┘ 
txt    └─────┘                └─┘       └┘ 
par    └─────┘                └─┘       └┘ 
pid    └───┘└┘                └─┘       └┘ 
st   ────────────────────────────────────────
375        (⨆ (k : ℕ) (h : ennreal_rat_embed k ≤ f a), ennreal_rat_embed k),
id                                                └───────────────┘
src  ─────┘ └────┘ └─────┘                     └───────────────┘ 
typ  ─────┘ └────┘ └─────┘                  └───────────────┘ 
doc  ─────┘ └────┘ └─────┘                     └───────────────┘ 
txt  ─────┘  └────┘ └─────┘                                        
par  ─────┘  └────┘ └─────┘                                        
pid  ─────┘  └────┘ └─────┘                                        
st   ─────────────────────────────────────────────────────────────────────┘└─
376    { refine le_supr_of_le (encodable.encode q) _,
id              └───────────┘  └──────────────┘ 
src      └─────┘└───────────┘ └──────────────┘ └─┘
typ      └─────┘└───────────┘ └──────────────┘└─┘
doc      └─────┘                               └─┘
txt      └─────┘                               └─┘
par      └─────┘                               └─┘
pid                                           └─┘
st   ───┘└─────────────────────────────────────────┘└─
377      rw [ennreal_rat_embed_encode q],
id           └──────────────────────┘ 
src      └──┘└──────────────────────┘ 
typ      └──┘└──────────────────────┘
doc      └──┘                         
txt      └──┘                         
par      └──┘                         
pid        └┘                         
st   ─────────────────────────────────┘└──
378      refine le_supr_of_le (le_of_lt q_lt) _,
id              └───────────┘  └──────┘ └──┘
src      └─────┘└───────────┘ └──────┘    └─┘
typ      └─────┘└───────────┘ └──────┘└──┘└─┘
doc      └─────┘                          └─┘
txt      └─────┘                          └─┘
par      └─────┘                          └─┘
pid                                      └─┘
st   ─────────────────────────────────────────┘└─
379      exact le_refl _ },
id             └─────┘
src      └────┘└─────┘└─┘
typ      └────┘└─────┘└─┘
doc      └────┘       └─┘
txt      └────┘       └─┘
par      └────┘       └─┘
pid                  └┘
st   ───────────────────┘└┘
380    exact lt_irrefl _ (lt_of_le_of_lt this lt_q)
id           └───────┘    └────────────┘ └──┘ └──┘
src    └────┘└───────┘└─┘ └────────────┘        └┘
typ    └────┘└───────┘└─┘ └────────────┘└──┘└──┘└┘
doc    └────┘         └─┘                       └┘
txt    └────┘         └─┘                       └┘
par    └────┘         └─┘                       └┘
pid                  └─┘                       
st   ──────────────────────────────────────────────┘
381  end
st   └─┘
382  
383  lemma eapprox_comp [measurable_space γ] {f : γ → ennreal} {g : α → γ} {n : ℕ}
id                       └──────────────┘           └─────┘                 
src                      └──────────────┘             └─────┘                   
typ                      └──────────────┘           └─────┘                 
doc                                                   └─────┘
384    (hf : _root_.measurable f) (hg : _root_.measurable g) :
id           └───────────────┘         └───────────────┘ 
src          └───────────────┘          └───────────────┘
typ          └───────────────┘         └───────────────┘ 
doc          └───────────────┘          └───────────────┘
385    (eapprox (f ∘ g) n : α → ennreal) = (eapprox f n : γ →ₛ ennreal) ∘ g :=
id      └─────┘            └─────┘    └─────┘      └┘ └─────┘   
src     └─────┘                └─────┘    └─────┘         └┘ └─────┘  
typ     └─────┘            └─────┘    └─────┘      └┘ └─────┘   
doc                             └─────┘                     └┘ └─────┘
386  funext $ assume a, approx_comp a hf hg
id   └────┘            └─────────┘  └┘ └┘
src  └────┘             └─────────┘
typ  └────┘            └─────────┘  └┘ └┘
387  
388  end eapprox
389  
390  end measurable
391  
392  section measure
393  variables [measure_space α]
id              └───────────┘
src             └───────────┘
typ             └───────────┘
doc             └───────────┘
394  
395  lemma volume_bUnion_preimage (s : finset β) (f : α →ₛ β) :
id                                     └────┘         └┘ 
src                                    └────┘           └┘
typ                                    └────┘         └┘ 
doc                                    └────┘           └┘
396    volume (⋃b ∈ s, f ⁻¹' {b}) = s.sum (λb, volume (f ⁻¹' {b})) :=
id     └────┘       └─┘     └──┘     └────┘   └─┘ 
src    └────┘          └─┘       └──┘      └────┘    └─┘ 
typ    └────┘       └─┘     └──┘     └────┘   └─┘ 
doc                    └─┘                             └─┘
397  begin
st   └─────
398    /- Taking advantage of the fact that `f ⁻¹' {b}` are disjoint for `b ∈ s`. -/
st   ────────────────────────────────────────────────────────────────────────────────
399    rw [volume_bUnion_finset],
id         └──────────────────┘
src    └──┘└──────────────────┘
typ    └──┘└──────────────────┘
doc    └──┘                    
txt    └──┘                    
par    └──┘                    
pid      └┘                    
st   ─────────────────────────┘└──
400    { simp only [pairwise_on, (on), finset.mem_coe, ne.def],
id                  └─────────┘       └────────────┘  └────┘
src      └─────────┘└─────────┘└┘└───┘└────────────┘└┘└────┘
typ      └─────────┘└─────────┘└┘└───┘└────────────┘└┘└────┘
doc      └─────────┘└─────────┘└┘ └───┘              └┘      
txt      └─────────┘           └┘ └───┘              └┘      
par      └─────────┘           └┘ └───┘              └┘      
pid          └──┘└┘           └┘ └───┘              └┘      
st   ───┘└───────────────────────────────────────────────────┘└─
401      rintros _ _ _ _ ne _ ⟨h₁, h₂⟩,
src      └───────────────────────────┘
typ      └───────────────────────────┘
doc      └───────────────────────────┘
txt      └───────────────────────────┘
par      └───────────────────────────┘
pid             └────────────────────┘
st   ────────────────────────────────┘└─
402      simp only [mem_singleton_iff, mem_preimage] at h₁ h₂,
id                  └───────────────┘  └──────────┘
src      └─────────┘└───────────────┘└┘└──────────┘└────────┘
typ      └─────────┘└───────────────┘└┘└──────────┘└────────┘
doc      └─────────┘                 └┘            └────────┘
txt      └─────────┘                 └┘            └────────┘
par      └─────────┘                 └┘            └────────┘
pid          └──┘└┘                 └┘            └──────┘
st   ───────────────────────────────────────────────────────┘└─
403      rw [← h₁, h₂] at ne,
id             └┘  └┘
src      └────┘  └┘  └─────┘
typ      └────┘└┘└┘└┘└─────┘
doc      └────┘  └┘  └─────┘
txt      └────┘  └┘  └─────┘
par      └────┘  └┘  └─────┘
pid        └──┘  └┘  └────┘
st   ───────────┘└──┘└────┘└─
404      exact ne rfl },
id             └┘ └─┘
src      └────┘└┘└─┘
typ      └────┘└┘└─┘
doc      └────┘     
txt      └────┘     
par      └────┘     
pid                
st   ────────────────┘└┘
405    exact assume a ha, preimage_measurable _ _
id                        └─────────────────┘
src    └────┘      └─────┘└─────────────────┘└───┘
typ    └────┘      └─────┘└─────────────────┘└───┘
doc    └────┘      └─────┘                   └───┘
txt    └────┘      └─────┘                   └───┘
par    └────┘      └─────┘                   └───┘
pid               └─────┘                   └──┘
st   ────────────────────────────────────────────┘
406  end
st   └─┘
407  
408  /-- Integral of a simple function whose codomain is `ennreal`. -/
409  def integral (f : α →ₛ ennreal) : ennreal :=
id                      └┘ └─────┘    └─────┘
src                      └┘ └─────┘    └─────┘
typ                     └┘ └─────┘    └─────┘
doc                      └┘ └─────┘    └─────┘
410  f.range.sum (λ x, x * volume (f ⁻¹' {x}))
id   └────┘└──┘        └────┘   └─┘ 
src   └────┘└──┘          └────┘    └─┘ 
typ  └────┘└──┘        └────┘   └─┘ 
doc   └────┘                         └─┘
411  
412  /-- Calculate the integral of `(g ∘ f)`, where `g : β → ennreal` and `f : α →ₛ β`.  -/
413  lemma map_integral (g : β → ennreal) (f : α →ₛ β) :
id                              └─────┘        └┘ 
src                              └─────┘         └┘
typ                             └─────┘        └┘ 
doc                              └─────┘         └┘
414    (f.map g).integral = f.range.sum (λ x, g x * volume (f ⁻¹' {x})) :=
id      └──┘  └──────┘   └────┘└──┘         └────┘   └─┘ 
src      └──┘   └──────┘    └────┘└──┘            └────┘    └─┘ 
typ     └──┘  └──────┘   └────┘└──┘         └────┘   └─┘ 
doc      └──┘   └──────┘     └────┘                           └─┘
415  begin
st   └─────
416    simp only [integral, range_map],
id                └──────┘  └───────┘
src    └─────────┘└──────┘└┘└───────┘
typ    └─────────┘└──────┘└┘└───────┘
doc    └─────────┘└──────┘└┘         
txt    └─────────┘        └┘         
par    └─────────┘        └┘         
pid        └──┘└┘        └┘         
st   ────────────────────────────────┘└─
417    refine finset.sum_image' _ (assume b hb, _),
id            └───────────────┘
src    └─────┘└───────────────┘└─┘       └───────┘
typ    └─────┘└───────────────┘└─┘       └───────┘
doc    └─────┘                 └─┘       └───────┘
txt    └─────┘                 └─┘       └───────┘
par    └─────┘                 └─┘       └───────┘
pid                           └─┘       └───────┘
st   ────────────────────────────────────────────┘└─
418    rcases mem_range.1 hb with ⟨a, rfl⟩,
id            └───────┘   └┘
src    └─────┘└───────┘└─┘  └────────────┘
typ    └─────┘└───────┘└─┘└┘└────────────┘
doc    └─────┘         └─┘  └────────────┘
txt    └─────┘         └─┘  └────────────┘
par    └─────┘         └─┘  └────────────┘
pid                   └─┘  └────────────┘
st   ────────────────────────────────────┘└─
419    rw [map_preimage_singleton, volume_bUnion_preimage, finset.mul_sum],
id         └────────────────────┘  └────────────────────┘  └────────────┘
src    └──┘└────────────────────┘└┘└────────────────────┘└┘└────────────┘
typ    └──┘└────────────────────┘└┘└────────────────────┘└┘└────────────┘
doc    └──┘                      └┘                      └┘              
txt    └──┘                      └┘                      └┘              
par    └──┘                      └┘                      └┘              
pid      └┘                      └┘                      └┘              
st   ───────────────────────────┘└──────────────────────┘└──────────────┘└──
420    refine finset.sum_congr _ _,
id            └──────────────┘
src    └─────┘└──────────────┘└──┘
typ    └─────┘└──────────────┘└──┘
doc    └─────┘                └──┘
txt    └─────┘                └──┘
par    └─────┘                └──┘
pid                          └──┘
st   ────────────────────────────┘└─
421    { congr },
src      └────┘
typ      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└────┘└┘
422    { assume x, simp only [finset.mem_filter], rintro ⟨_, h⟩, rw h }
id                            └───────────────┘                     
src      └──────┘  └─────────┘└───────────────┘  └───────────┘  └─┘ 
typ      └──────┘  └─────────┘└───────────────┘  └───────────┘  └─┘
doc      └──────┘  └─────────┘                   └───────────┘  └─┘ 
txt      └──────┘  └─────────┘                   └───────────┘  └─┘ 
par      └──────┘  └─────────┘                   └───────────┘  └─┘ 
pid      └──────┘      └──┘└┘                         └─────┘     
st   ───────────┘└─────────────────────────────┘└─────────────┘└─────┘└─
423  end
st   ──┘
424  
425  lemma zero_integral : (0 : α →ₛ ennreal).integral = 0 :=
id                               └┘ └─────┘ └──────┘  
src                               └┘ └─────┘ └──────┘  
typ                              └┘ └─────┘ └──────┘  
doc                               └┘ └─────┘ └──────┘
426  begin
st   └─────
427    refine (finset.sum_eq_zero_iff_of_nonneg $ assume _ _, zero_le _).2 _,
id             └──────────────────────────────┘               └─────┘
src    └─────┘ └──────────────────────────────┘       └────┘└─────┘└─────┘
typ    └─────┘ └──────────────────────────────┘       └────┘└─────┘└─────┘
doc    └─────┘                                        └────┘       └─────┘
txt    └─────┘                                        └────┘       └─────┘
par    └─────┘                                        └────┘       └─────┘
pid                                                  └────┘       └─────┘
st   ──────────────────────────────────────────────────────────────────────┘└─
428    assume r hr, rcases mem_range.1 hr with ⟨a, rfl⟩,
id                         └───────┘   └┘
src    └─────────┘  └─────┘└───────┘└─┘  └────────────┘
typ    └─────────┘  └─────┘└───────┘└─┘└┘└────────────┘
doc    └─────────┘  └─────┘         └─┘  └────────────┘
txt    └─────────┘  └─────┘         └─┘  └────────────┘
par    └─────────┘  └─────┘         └─┘  └────────────┘
pid    └─────────┘                 └─┘  └────────────┘
st   ────────────┘└───────────────────────────────────┘└─
429    exact zero_mul _
id           └──────┘
src    └────┘└──────┘└─┘
typ    └────┘└──────┘└─┘
doc    └────┘        └─┘
txt    └────┘        └─┘
par    └────┘        └─┘
pid                 └┘
st   ──────────────────┘
430  end
st   └─┘
431  
432  lemma add_integral (f g : α →ₛ ennreal) : (f + g).integral = f.integral + g.integral :=
id                              └┘ └─────┘        └──────┘   └───────┘  └───────┘
src                              └┘ └─────┘          └──────┘    └───────┘   └───────┘
typ                             └┘ └─────┘        └──────┘   └───────┘  └───────┘
doc                              └┘ └─────┘           └──────┘     └───────┘    └───────┘
433  calc (f + g).integral =
id            └──────┘
src             └──────┘
typ           └──────┘
doc              └──────┘
434        (pair f g).range.sum (λx, x.1 * volume (pair f g ⁻¹' {x}) + x.2  * volume (pair f g ⁻¹' {x})) :
id          └──┘   └───┘ └─┘         └────┘  └──┘   └─┘         └────┘  └──┘   └─┘ 
src         └──┘     └───┘ └─┘           └────┘  └──┘     └─┘           └────┘  └──┘     └─┘ 
typ         └──┘   └───┘ └─┘         └────┘  └──┘   └─┘         └────┘  └──┘   └─┘ 
doc         └──┘     └───┘                         └──┘     └─┘                       └──┘     └─┘
435      by rw [add_eq_map₂, map_integral]; exact finset.sum_congr rfl (assume a ha, add_mul _ _ _)
id              └─────────┘  └──────────┘         └──────────────┘ └─┘               └─────┘
src         └──┘└─────────┘└┘└──────────┘  └────┘└──────────────┘└─┘       └─────┘└─────┘└───────
typ         └──┘└─────────┘└┘└──────────┘  └────┘└──────────────┘└─┘       └─────┘└─────┘└───────
doc         └──┘           └┘└──────────┘  └────┘                          └─────┘       └───────
txt         └──┘           └┘              └────┘                          └─────┘       └───────
par         └──┘           └┘              └────┘                          └─────┘       └───────
pid           └┘           └┘                                             └─────┘       └─────┘
st         └──────────────┘└────────────┘└─────────────────────────────────────────────────────────
436    ... = (pair f g).range.sum (λx, x.1 * volume (pair f g ⁻¹' {x})) +
id            └──┘   └───┘ └─┘         └────┘  └──┘   └─┘     
src  ─┘       └──┘     └───┘ └─┘           └────┘  └──┘     └─┘      
typ  ─┘       └──┘   └───┘ └─┘         └────┘  └──┘   └─┘     
doc  ─┘       └──┘     └───┘                         └──┘     └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
437        (pair f g).range.sum (λx, x.2 * volume (pair f g ⁻¹' {x})) : by rw [finset.sum_add_distrib]
id          └──┘   └───┘ └─┘         └────┘  └──┘   └─┘              └────────────────────┘
src         └──┘     └───┘ └─┘           └────┘  └──┘     └─┘           └──┘└────────────────────┘└─
typ         └──┘   └───┘ └─┘         └────┘  └──┘   └─┘          └──┘└────────────────────┘└─
doc         └──┘     └───┘                         └──┘     └─┘            └──┘                      └─
txt                                                                        └──┘                      └─
par                                                                        └──┘                      └─
pid                                                                          └┘                      
st                                                                        └─────────────────────────┘
438    ... = ((pair f g).map prod.fst).integral + ((pair f g).map prod.snd).integral :
id             └──┘   └─┘  └──────┘ └──────┘     └──┘   └─┘  └──────┘ └──────┘
src  ─┘        └──┘     └─┘  └──────┘ └──────┘     └──┘     └─┘  └──────┘ └──────┘
typ  ─┘        └──┘   └─┘  └──────┘ └──────┘     └──┘   └─┘  └──────┘ └──────┘
doc  ─┘        └──┘     └─┘           └──────┘      └──┘     └─┘           └──────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
439      by rw [map_integral, map_integral]
id              └──────────┘  └──────────┘
src         └──┘└──────────┘└┘└──────────┘└─
typ         └──┘└──────────┘└┘└──────────┘└─
doc         └──┘└──────────┘└┘└──────────┘└─
txt         └──┘            └┘            └─
par         └──┘            └┘            └─
pid           └┘            └┘            
st         └───────────────┘└────────────┘
440    ... = integral f + integral g : rfl
id           └──────┘   └──────┘    └─┘
src  ─┘      └──────┘    └──────┘     └─┘
typ  ─┘      └──────┘   └──────┘    └─┘
doc  ─┘      └──────┘     └──────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
441  
442  lemma const_mul_integral (f : α →ₛ ennreal) (x : ennreal) :
id                                  └┘ └─────┘       └─────┘
src                                  └┘ └─────┘       └─────┘
typ                                 └┘ └─────┘       └─────┘
doc                                  └┘ └─────┘       └─────┘
443    (const α x * f).integral = x * f.integral :=
id      └───┘     └──────┘     └───────┘
src     └───┘        └──────┘       └───────┘
typ     └───┘     └──────┘     └───────┘
doc     └───┘         └──────┘         └───────┘
444  calc (f.map (λa, x * a)).integral = f.range.sum (λr, x * r * volume (f ⁻¹' {r})) :
id         └──┘         └──────┘    └────┘└──┘         └────┘   └─┘ 
src         └──┘            └──────┘     └────┘└──┘            └────┘    └─┘ 
typ        └──┘         └──────┘    └────┘└──┘         └────┘   └─┘ 
doc         └──┘             └──────┘     └────┘                            └─┘
445      by rw [map_integral]
id              └──────────┘
src         └──┘└──────────┘└─
typ         └──┘└──────────┘└─
doc         └──┘└──────────┘└─
txt         └──┘            └─
par         └──┘            └─
pid           └┘            
st         └───────────────┘
446    ... = f.range.sum (λr, x * (r * volume (f ⁻¹' {r}))) :
id           └────┘└──┘          └────┘   └─┘ 
src  ─┘       └────┘└──┘             └────┘    └─┘ 
typ  ─┘      └────┘└──┘          └────┘   └─┘ 
doc  ─┘       └────┘                             └─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
447      finset.sum_congr rfl (assume a ha, mul_assoc _ _ _)
id       └──────────────┘ └─┘          └┘  └───────┘
src      └──────────────┘ └─┘               └───────┘
typ      └──────────────┘ └─┘          └┘  └───────┘
448    ... = x * f.integral :
id             └───────┘
src              └───────┘
typ            └───────┘
doc               └───────┘
449      finset.mul_sum.symm
id       └────────────┘└───┘
src      └────────────┘└───┘
typ      └────────────┘└───┘
450  
451  lemma mem_restrict_range [has_zero β] {r : β} {s : set α} {f : α →ₛ β} (hs : is_measurable s) :
id                             └──────┘               └─┘         └┘         └───────────┘ 
src                            └──────┘                 └─┘           └┘          └───────────┘
typ                            └──────┘               └─┘         └┘         └───────────┘ 
doc                                                                   └┘          └───────────┘
452    r ∈ (restrict f s).range ↔ (r = 0 ∧ s ≠ univ) ∨ (∃a∈s, f a = r) :=
id        └──────┘   └───┘           └──┘         
src        └──────┘     └───┘             └──┘           
typ       └──────┘   └───┘           └──┘         
doc         └──────┘     └───┘
453  begin
st   └─────
454    simp only [mem_range, restrict_apply, hs],
id                └───────┘  └────────────┘  └┘
src    └─────────┘└───────┘└┘└────────────┘└┘  
typ    └─────────┘└───────┘└┘└────────────┘└┘└┘
doc    └─────────┘         └┘              └┘  
txt    └─────────┘         └┘              └┘  
par    └─────────┘         └┘              └┘  
pid        └──┘└┘         └┘              └┘  
st   ──────────────────────────────────────────┘└─
455    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
456    { rintros ⟨a, ha⟩,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid             └──────┘
st   ───┘└─────────────┘└─
457      split_ifs at ha,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid               └────┘
st   ──────────────────┘└─
458      { exact or.inr ⟨a, h, ha⟩ },
id               └────┘      └┘
src        └────┘└────┘  └┘ └┘  └┘
typ        └────┘└────┘ └┘└┘└┘└┘
doc        └────┘        └┘ └┘  └┘
txt        └────┘        └┘ └┘  └┘
par        └────┘        └┘ └┘  └┘
pid                     └┘ └┘  
st   ─────┘└──────────────────────┘└┘
459      { exact or.inl ⟨ha.symm, assume eq, h $ eq.symm ▸ trivial⟩ } },
id               └────┘  └─────┘                  └───┘  └─────┘
src        └────┘└────┘ └─────┘└┘      └───┘    └───┘└─────┘└┘
typ        └────┘└────┘ └─────┘└┘      └───┘   └───┘└─────┘└┘
doc        └────┘              └┘      └───┘                 └┘
txt        └────┘              └┘      └───┘                 └┘
par        └────┘              └┘      └───┘                 └┘
pid                           └┘      └───┘                 
st   ──────────────────────────────────────────────────────────────┘└──┘
460    { rintros (⟨rfl, h⟩ | ⟨a, ha, rfl⟩),
src      └───────────────────────────────┘
typ      └───────────────────────────────┘
doc      └───────────────────────────────┘
txt      └───────────────────────────────┘
par      └───────────────────────────────┘
pid             └────────────────────────┘
st   ────────────────────────────────────┘└─
461      { have : ¬ ∀a, a ∈ s := assume this, h $ eq_univ_of_forall this,
id                                             └───────────────┘
src        └─────┘     └──┘      └─────┘  └───────────────┘
typ        └─────┘    └──┘      └─────┘ └───────────────┘
doc        └─────┘      └──┘      └─────┘                   
txt        └─────┘      └──┘      └─────┘                   
par        └─────┘      └──┘      └─────┘                   
pid        └───┘└┘      └──┘      └─────┘                   
st   ─────┘└───────────────────────────────────────────────────────────┘└─
462        rcases not_forall.1 this with ⟨a, ha⟩,
id                └────────┘   └──┘
src        └─────┘└────────┘└─┘    └───────────┘
typ        └─────┘└────────┘└─┘└──┘└───────────┘
doc        └─────┘          └─┘    └───────────┘
txt        └─────┘          └─┘    └───────────┘
par        └─────┘          └─┘    └───────────┘
pid                        └─┘    └───────────┘
st   ──────────────────────────────────────────┘└─
463        refine ⟨a, _⟩,
id                 
src        └─────┘  └──┘
typ        └─────┘ └──┘
doc        └─────┘  └──┘
txt        └─────┘  └──┘
par        └─────┘  └──┘
pid                └──┘
st   ──────────────────┘└─
464        rw [if_neg ha] },
id             └────┘ └┘
src        └──┘└────┘  └┘
typ        └──┘└────┘└┘└┘
doc        └──┘        └┘
txt        └──┘        └┘
par        └──┘        └┘
pid          └┘        
st   ──────────────────┘└┘
465      { refine ⟨a, _⟩,
id                 
src        └─────┘  └──┘
typ        └─────┘ └──┘
doc        └─────┘  └──┘
txt        └─────┘  └──┘
par        └─────┘  └──┘
pid                └──┘
st   ──────────────────┘└─
466        rw [if_pos ha] } }
id             └────┘ └┘
src        └──┘└────┘  └┘
typ        └──┘└────┘└┘└┘
doc        └──┘        └┘
txt        └──┘        └┘
par        └──┘        └┘
pid          └┘        
st   ──────────────────┘└───
467  end
st   ──┘
468  
469  lemma restrict_preimage' {r : ennreal} {s : set α}
id                                 └─────┘       └─┘ 
src                                └─────┘       └─┘
typ                                └─────┘       └─┘ 
doc                                └─────┘
470    (f : α →ₛ ennreal) (hs : is_measurable s) (hr : r ≠ 0) :
id           └┘ └─────┘        └───────────┘          
src           └┘ └─────┘        └───────────┘            
typ          └┘ └─────┘        └───────────┘          
doc           └┘ └─────┘        └───────────┘
471    (restrict f s) ⁻¹' {r} = (f ⁻¹' {r} ∩ s) :=
id      └──────┘    └─┘      └─┘    
src     └──────┘      └─┘        └─┘    
typ     └──────┘    └─┘      └─┘    
doc     └──────┘      └─┘          └─┘
472  begin
st   └─────
473    ext a,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
474    by_cases a ∈ s; simp [hs, h, hr.symm]
id                        └┘  
src    └───────┘    └────┘  └┘ └┘       └┘
typ    └───────┘  └────┘└┘└┘└┘└─────┘└┘
doc    └───────┘     └────┘  └┘ └┘       └┘
txt    └───────┘     └────┘  └┘ └┘       └┘
par    └───────┘     └────┘  └┘ └┘       └┘
pid                       └┘ └┘       
st   ───────────────────────────────────────┘
475  end
st   └─┘
476  
477  lemma restrict_integral (f : α →ₛ ennreal) (s : set α) (hs : is_measurable s) :
id                                 └┘ └─────┘       └─┘         └───────────┘ 
src                                 └┘ └─────┘       └─┘          └───────────┘
typ                                └┘ └─────┘       └─┘         └───────────┘ 
doc                                 └┘ └─────┘                    └───────────┘
478    (restrict f s).integral = f.range.sum (λr, r * volume (f ⁻¹' {r} ∩ s)) :=
id      └──────┘   └──────┘   └────┘└──┘       └────┘   └─┘    
src     └──────┘     └──────┘    └────┘└──┘         └────┘    └─┘    
typ     └──────┘   └──────┘   └────┘└──┘       └────┘   └─┘    
doc     └──────┘     └──────┘     └────┘                        └─┘
479  begin
st   └─────
480    refine finset.sum_bij_ne_zero (λr _ _, r) _ _ _ _,
id            └────────────────────┘
src    └─────┘└────────────────────┘  └─────┘ └───────┘
typ    └─────┘└────────────────────┘  └─────┘ └───────┘
doc    └─────┘                        └─────┘ └───────┘
txt    └─────┘                        └─────┘ └───────┘
par    └─────┘                        └─────┘ └───────┘
pid                                  └─────┘ └───────┘
st   ──────────────────────────────────────────────────┘└─
481    { assume r hr,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
482      rcases (mem_restrict_range hs).1 hr with ⟨rfl, h⟩ | ⟨a, ha, rfl⟩,
id               └────────────────┘ └┘    └┘
src      └─────┘ └────────────────┘  └──┘  └───────────────────────────┘
typ      └─────┘ └────────────────┘└┘└──┘└┘└───────────────────────────┘
doc      └─────┘                     └──┘  └───────────────────────────┘
txt      └─────┘                     └──┘  └───────────────────────────┘
par      └─────┘                     └──┘  └───────────────────────────┘
pid                                 └──┘  └───────────────────────────┘
st   ───────────────────────────────────────────────────────────────────┘└─
483      { simp },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ─────┘└───┘└┘
484      { assume _, exact mem_range.2 ⟨a, rfl⟩ } },
id                         └───────┘      └─┘
src        └──────┘  └────┘└───────┘└─┘  └┘└─┘└┘
typ        └──────┘  └────┘└───────┘└─┘ └┘└─┘└┘
doc        └──────┘  └────┘         └─┘  └┘   └┘
txt        └──────┘  └────┘         └─┘  └┘   └┘
par        └──────┘  └────┘         └─┘  └┘   └┘
pid        └──────┘                └─┘  └┘   
st   ─────────────┘└───────────────────────────┘└──┘
485    { assume a b _ _ _ _ h, exact h },
id                                   
src      └──────────────────┘  └────┘ 
typ      └──────────────────┘  └────┘
doc      └──────────────────┘  └────┘ 
txt      └──────────────────┘  └────┘ 
par      └──────────────────┘  └────┘ 
pid      └──────────────────┘        
st   ───┘└──────────────────┘└────────┘└┘
486    { assume r hr,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
487      by_cases r0 : r = 0, { simp [r0] },
id                                  └┘
src      └───────┘  └─┘ └┘    └────┘  └┘
typ      └───────┘  └─┘└┘    └────┘└┘└┘
doc      └───────┘  └─┘  └┘    └────┘  └┘
txt      └───────┘  └─┘  └┘    └────┘  └┘
par      └───────┘  └─┘  └┘    └────┘  └┘
pid                └─┘            
st   ──────────────────────┘└──┘└────────┘└┘
488      assume h0,
src      └───────┘
typ      └───────┘
doc      └───────┘
txt      └───────┘
par      └───────┘
pid      └───────┘
st   ────────────┘└─
489      rcases mem_range.1 hr with ⟨a, rfl⟩,
id              └───────┘   └┘
src      └─────┘└───────┘└─┘  └────────────┘
typ      └─────┘└───────┘└─┘└┘└────────────┘
doc      └─────┘         └─┘  └────────────┘
txt      └─────┘         └─┘  └────────────┘
par      └─────┘         └─┘  └────────────┘
pid                     └─┘  └────────────┘
st   ──────────────────────────────────────┘└─
490      have : f ⁻¹' {f a} ∩ s ≠ ∅,
id                └─┘        
src      └─────┘ └─┘└┘ └┘ 
typ      └─────┘ └─┘└┘└┘
doc      └─────┘ └─┘ └┘ └┘   
txt      └─────┘     └┘ └┘   
par      └─────┘     └┘ └┘   
pid      └───┘└┘     └┘ └┘   
st   ─────────────────────────────┘└─
491      { assume h, simpa [h] using h0 },
id                                  └┘
src        └──────┘  └─────┘ └──────┘  
typ        └──────┘  └─────┘└──────┘└┘
doc        └──────┘  └─────┘ └──────┘  
txt        └──────┘  └─────┘ └──────┘  
par        └──────┘  └─────┘ └──────┘  
pid        └──────┘        └────┘  
st   ─────┘└──────┘└───────────────────┘└┘
492      rcases ne_empty_iff_nonempty.1 this with ⟨a', eq', ha'⟩,
id              └───────────────────┘   └──┘
src      └─────┘└───────────────────┘└─┘    └──────────────────┘
typ      └─────┘└───────────────────┘└─┘└──┘└──────────────────┘
doc      └─────┘                     └─┘    └──────────────────┘
txt      └─────┘                     └─┘    └──────────────────┘
par      └─────┘                     └─┘    └──────────────────┘
pid                                 └─┘    └──────────────────┘
st   ──────────────────────────────────────────────────────────┘└─
493      refine ⟨_, (mem_restrict_range hs).2 (or.inr ⟨a', ha', _⟩), _, rfl⟩,
id                   └────────────────┘ └┘     └────┘  └┘  └─┘          └─┘
src      └─────┘ └─┘ └────────────────┘  └──┘ └────┘   └┘   └────────┘└─┘
typ      └─────┘ └─┘ └────────────────┘└┘└──┘ └────┘ └┘└┘└─┘└────────┘└─┘
doc      └─────┘ └─┘                     └──┘          └┘   └────────┘   
txt      └─────┘ └─┘                     └──┘          └┘   └────────┘   
par      └─────┘ └─┘                     └──┘          └┘   └────────┘   
pid             └─┘                     └──┘          └┘   └────────┘   
st   ──────────────────────────────────────────────────────────────────────┘└─
494      { simpa using eq' },
id                     └─┘
src        └──────────┘   
typ        └──────────┘└─┘
doc        └──────────┘   
txt        └──────────┘   
par        └──────────┘   
pid             └────┘   
st   ─────┘└──────────────┘└┘
495      { rwa [restrict_preimage' _ hs r0] } },
id              └────────────────┘   └┘ └┘
src        └───┘└────────────────┘└─┘    └┘
typ        └───┘└────────────────┘└─┘└┘└┘└┘
doc        └───┘                  └─┘    └┘
txt        └───┘                  └─┘    └┘
par        └───┘                  └─┘    └┘
pid           └┘                  └─┘    
st   ────────────────────────────────────┘└──┘
496    { assume r hr ne,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ─────────────────┘└─
497      by_cases r = 0, { simp [h] },
id                              
src      └───────┘  └┘    └────┘ └┘
typ      └───────┘ └┘    └────┘└┘
doc      └───────┘  └┘    └────┘ └┘
txt      └───────┘  └┘    └────┘ └┘
par      └───────┘  └┘    └────┘ └┘
pid                         
st   ─────────────────┘└──┘└───────┘└┘
498      rw [restrict_preimage' _ hs h] }
id           └────────────────┘   └┘ 
src      └──┘└────────────────┘└─┘   └┘
typ      └──┘└────────────────┘└─┘└┘└┘
doc      └──┘                  └─┘   └┘
txt      └──┘                  └─┘   └┘
par      └──┘                  └─┘   └┘
pid        └┘                  └─┘   
st   ────────────────────────────────┘└─
499  end
st   ──┘
500  
501  lemma restrict_const_integral (c : ennreal) (s : set α) (hs : is_measurable s) :
id                                      └─────┘       └─┘         └───────────┘ 
src                                     └─────┘       └─┘          └───────────┘
typ                                     └─────┘       └─┘         └───────────┘ 
doc                                     └─────┘                    └───────────┘
502    (restrict (const α c) s).integral = c * volume s :=
id      └──────┘  └───┘     └──────┘     └────┘ 
src     └──────┘  └───┘        └──────┘      └────┘
typ     └──────┘  └───┘     └──────┘     └────┘ 
doc     └──────┘  └───┘        └──────┘
503  have (@const α ennreal _ c) ⁻¹' {c} = univ,
id          └───┘  └─────┘     └─┘    └──┘
src         └───┘   └─────┘      └─┘     └──┘
typ         └───┘  └─────┘     └─┘    └──┘
doc         └───┘   └─────┘      └─┘
504  begin
st   └─────
505    refine eq_univ_of_forall (assume a, _),
id            └───────────────┘
src    └─────┘└───────────────┘       └────┘
typ    └─────┘└───────────────┘       └────┘
doc    └─────┘                        └────┘
txt    └─────┘                        └────┘
par    └─────┘                        └────┘
pid                                  └────┘
st   ───────────────────────────────────────┘└─
506    simp,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
507  end,
st   ──┘
508  calc (restrict (const α c) s).integral = c * volume ((const α c) ⁻¹' {c} ∩ s) :
id         └──────┘  └───┘     └──────┘      └────┘   └───┘    └─┘    
src        └──────┘  └───┘        └──────┘       └────┘   └───┘      └─┘    
typ        └──────┘  └───┘     └──────┘      └────┘   └───┘    └─┘    
doc        └──────┘  └───┘        └──────┘                 └───┘      └─┘
509    begin
st     └─────
510      rw [restrict_integral (const α c) s hs],
id           └───────────────┘  └───┘     └┘
src      └──┘└───────────────┘ └───┘  └┘   
typ      └──┘└───────────────┘ └───┘└┘└┘
doc      └──┘                  └───┘  └┘   
txt      └──┘                         └┘   
par      └──┘                         └┘   
pid        └┘                         └┘   
st   ─────────────────────────────────────────┘└──
511      refine finset.sum_eq_single c _ _,
id              └──────────────────┘ 
src      └─────┘└──────────────────┘ └──┘
typ      └─────┘└──────────────────┘└──┘
doc      └─────┘                     └──┘
txt      └─────┘                     └──┘
par      └─────┘                     └──┘
pid                                 └──┘
st   ────────────────────────────────────┘└─
512      { assume r hr, rcases mem_range.1 hr with ⟨a, rfl⟩, contradiction },
id                             └───────┘   └┘
src        └─────────┘  └─────┘└───────┘└─┘  └────────────┘  └────────────┘
typ        └─────────┘  └─────┘└───────┘└─┘└┘└────────────┘  └────────────┘
doc        └─────────┘  └─────┘         └─┘  └────────────┘  └────────────┘
txt        └─────────┘  └─────┘         └─┘  └────────────┘  └────────────┘
par        └─────────┘  └─────┘         └─┘  └────────────┘  └────────────┘
pid        └─────────┘                 └─┘  └────────────┘               
st   ─────┘└─────────┘└───────────────────────────────────┘└──────────────┘└┘
513      { by_cases nonempty α,
id                  └──────┘ 
src        └───────┘└──────┘
typ        └───────┘└──────┘
doc        └───────┘        
txt        └───────┘        
par        └───────┘        
pid                        
st   ────────────────────────┘└─
514        { assume ne,
src          └───────┘
typ          └───────┘
doc          └───────┘
txt          └───────┘
par          └───────┘
pid          └───────┘
st   ───────┘└───────┘└─
515          rcases h with ⟨a⟩,
id                  
src          └─────┘ └───────┘
typ          └─────┘└───────┘
doc          └─────┘ └───────┘
txt          └─────┘ └───────┘
par          └─────┘ └───────┘
pid                 └───────┘
st   ────────────────────────┘└─
516          exfalso,
src          └─────┘
typ          └─────┘
doc          └─────┘
txt          └─────┘
par          └─────┘
st   ──────────────┘└─
517          exact ne (mem_range.2 ⟨a, rfl⟩) },
id                 └┘  └───────┘      └─┘
src          └────┘└┘ └───────┘└─┘  └┘└─┘└─┘
typ          └────┘└┘ └───────┘└─┘ └┘└─┘└─┘
doc          └────┘            └─┘  └┘   └─┘
txt          └────┘            └─┘  └┘   └─┘
par          └────┘            └─┘  └┘   └─┘
pid                           └─┘  └┘   └┘
st   ───────────────────────────────────────┘└┘
518        { assume empty,
src          └──────────┘
typ          └──────────┘
doc          └──────────┘
txt          └──────────┘
par          └──────────┘
pid          └──────────┘
st   ───────────────────┘└─
519          have : (@const α ennreal _ c) ⁻¹' {c} ∩ s = ∅,
id                    └───┘  └─────┘      └─┘       
src          └─────┘  └───┘ └─────┘└─┘ └┘└─┘└─┘ 
typ          └─────┘  └───┘└─────┘└─┘ └┘└─┘└─┘
doc          └─────┘  └───┘ └─────┘└─┘ └┘└─┘ └─┘   
txt          └─────┘               └─┘ └┘    └─┘   
par          └─────┘               └─┘ └┘    └─┘   
pid          └───┘└┘               └─┘ └┘    └─┘   
st   ────────────────────────────────────────────────────┘└─
520          { ext a, exfalso, exact h ⟨a⟩ },
id                                     
src            └───┘  └─────┘  └────┘   └┘
typ            └───┘  └─────┘  └────┘ └┘
doc            └───┘  └─────┘  └────┘   └┘
txt            └───┘  └─────┘  └────┘   └┘
par            └───┘  └─────┘  └────┘   └┘
pid               └┘                   
st   ─────────┘└───┘└───────┘└────────────┘└┘
521          simp only [this, volume_empty, mul_zero] } }
id                      └──┘  └──────────┘  └──────┘
src          └─────────┘    └┘└──────────┘└┘└──────┘└┘
typ          └─────────┘└──┘└┘└──────────┘└┘└──────┘└┘
doc          └─────────┘    └┘            └┘        └┘
txt          └─────────┘    └┘            └┘        └┘
par          └─────────┘    └┘            └┘        └┘
pid              └──┘└┘    └┘            └┘        
st   ────────────────────────────────────────────────┘└───
522    end
st   ────┘
523    ... = c * volume s : by rw [this, univ_inter]
id             └────┘           └──┘  └────────┘
src             └────┘        └──┘    └┘└────────┘└─
typ            └────┘       └──┘└──┘└┘└────────┘└─
doc                            └──┘    └┘          └─
txt                            └──┘    └┘          └─
par                            └──┘    └┘          └─
pid                              └┘    └┘          
st                            └───────┘└──────────┘
524  
src  
typ  
doc  
txt  
par  
pid  
st   
525  lemma integral_sup_le (f g : α →ₛ ennreal) : f.integral ⊔ g.integral ≤ (f ⊔ g).integral :=
id                                 └┘ └─────┘    └───────┘  └───────┘      └──────┘
src                                 └┘ └─────┘     └───────┘   └───────┘        └──────┘
typ                                └┘ └─────┘    └───────┘  └───────┘      └──────┘
doc                                 └┘ └─────┘     └───────┘    └───────┘          └──────┘
526  calc f.integral ⊔ g.integral =
id        └───────┘  └───────┘
src        └───────┘   └───────┘
typ       └───────┘  └───────┘
doc        └───────┘    └───────┘
527        ((pair f g).map prod.fst).integral ⊔ ((pair f g).map prod.snd).integral : rfl
id           └──┘   └─┘  └──────┘ └──────┘     └──┘   └─┘  └──────┘ └──────┘    └─┘
src          └──┘     └─┘  └──────┘ └──────┘     └──┘     └─┘  └──────┘ └──────┘    └─┘
typ          └──┘   └─┘  └──────┘ └──────┘     └──┘   └─┘  └──────┘ └──────┘    └─┘
doc          └──┘     └─┘           └──────┘      └──┘     └─┘           └──────┘
528    ... ≤ (pair f g).range.sum (λx, (x.1 ⊔ x.2) * volume (pair f g ⁻¹' {x})) :
id            └──┘   └───┘ └─┘              └────┘  └──┘   └─┘ 
src           └──┘     └───┘ └─┘                 └────┘  └──┘     └─┘ 
typ           └──┘   └───┘ └─┘              └────┘  └──┘   └─┘ 
doc           └──┘     └───┘                                 └──┘     └─┘
529    begin
st     └─────
530      rw [map_integral, map_integral],
id           └──────────┘  └──────────┘
src      └──┘└──────────┘└┘└──────────┘
typ      └──┘└──────────┘└┘└──────────┘
doc      └──┘└──────────┘└┘└──────────┘
txt      └──┘            └┘            
par      └──┘            └┘            
pid        └┘            └┘            
st   ───────────────────┘└────────────┘└──
531      refine sup_le _ _;
id              └────┘
src      └─────┘└────┘└──┘
typ      └─────┘└────┘└──┘
doc      └─────┘      └──┘
txt      └─────┘      └──┘
par      └─────┘      └──┘
pid                  └──┘
st   ───────────────────────
532        refine finset.sum_le_sum (λ a _, canonically_ordered_semiring.mul_le_mul _ (le_refl _)),
id                └───────────────┘         └─────────────────────────────────────┘    └─────┘
src        └─────┘└───────────────┘  └────┘└─────────────────────────────────────┘└─┘ └─────┘└──┘
typ        └─────┘└───────────────┘  └────┘└─────────────────────────────────────┘└─┘ └─────┘└──┘
doc        └─────┘                   └────┘                                       └─┘        └──┘
txt        └─────┘                   └────┘                                       └─┘        └──┘
par        └─────┘                   └────┘                                       └─┘        └──┘
pid                                 └────┘                                       └─┘        └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
533      exact le_sup_left,
id             └─────────┘
src      └────┘└─────────┘
typ      └────┘└─────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ────────────────────┘└─
534      exact le_sup_right
id             └──────────┘
src      └────┘└──────────┘
typ      └────┘└──────────┘
doc      └────┘            
txt      └────┘            
par      └────┘            
pid                       
st   ───────────────────────
535    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
536    ... = (f ⊔ g).integral : by rw [sup_eq_map₂, map_integral]
id               └──────┘           └─────────┘  └──────────┘
src                └──────┘       └──┘└─────────┘└┘└──────────┘└─
typ              └──────┘       └──┘└─────────┘└┘└──────────┘└─
doc                 └──────┘       └──┘           └┘└──────────┘└─
txt                                └──┘           └┘            └─
par                                └──┘           └┘            └─
pid                                  └┘           └┘            
st                                └──────────────┘└────────────┘
537  
src  
typ  
doc  
txt  
par  
pid  
st   
538  lemma integral_le_integral (f g : α →ₛ ennreal) (h : f ≤ g) : f.integral ≤ g.integral :=
id                                      └┘ └─────┘             └───────┘  └───────┘
src                                      └┘ └─────┘                └───────┘   └───────┘
typ                                     └┘ └─────┘             └───────┘  └───────┘
doc                                      └┘ └─────┘                 └───────┘    └───────┘
539  calc f.integral ≤ f.integral ⊔ g.integral : le_sup_left
id        └───────┘   └───────┘  └───────┘   └─────────┘
src        └───────┘    └───────┘   └───────┘   └─────────┘
typ       └───────┘   └───────┘  └───────┘   └─────────┘
doc        └───────┘    └───────┘    └───────┘
540    ... ≤ (f ⊔ g).integral : integral_sup_le _ _
id               └──────┘    └─────────────┘
src                └──────┘    └─────────────┘
typ              └──────┘    └─────────────┘
doc                 └──────┘
541    ... = g.integral : by rw [sup_of_le_right h]
id           └───────┘          └─────────────┘ 
src           └───────┘      └──┘└─────────────┘ └─
typ          └───────┘      └──┘└─────────────┘└─
doc           └───────┘      └──┘                └─
txt                          └──┘                └─
par                          └──┘                └─
pid                            └┘                
st                          └────────────────────┘
542  
src  
typ  
doc  
txt  
par  
pid  
st   
543  lemma integral_congr (f g : α →ₛ ennreal) (h : ∀ₘ a, f a = g a) :
id                                └┘ └─────┘       └┘      
src                                └┘ └─────┘       └┘       
typ                               └┘ └─────┘       └┘      
doc                                └┘ └─────┘       └┘  
544    f.integral = g.integral :=
id     └───────┘  └───────┘
src     └───────┘   └───────┘
typ    └───────┘  └───────┘
doc     └───────┘    └───────┘
545  show ((pair f g).map prod.fst).integral = ((pair f g).map prod.snd).integral, from
id          └──┘   └─┘  └──────┘ └──────┘     └──┘   └─┘  └──────┘ └──────┘
src         └──┘     └─┘  └──────┘ └──────┘     └──┘     └─┘  └──────┘ └──────┘
typ         └──┘   └─┘  └──────┘ └──────┘     └──┘   └─┘  └──────┘ └──────┘
doc         └──┘     └─┘           └──────┘      └──┘     └─┘           └──────┘
546  begin
st   └─────
547    rw [map_integral, map_integral],
id         └──────────┘  └──────────┘
src    └──┘└──────────┘└┘└──────────┘
typ    └──┘└──────────┘└┘└──────────┘
doc    └──┘└──────────┘└┘└──────────┘
txt    └──┘            └┘            
par    └──┘            └┘            
pid      └┘            └┘            
st   ─────────────────┘└────────────┘└──
548    refine finset.sum_congr rfl (assume p hp, _),
id            └──────────────┘ └─┘
src    └─────┘└──────────────┘└─┘       └───────┘
typ    └─────┘└──────────────┘└─┘       └───────┘
doc    └─────┘                          └───────┘
txt    └─────┘                          └───────┘
par    └─────┘                          └───────┘
pid                                    └───────┘
st   ─────────────────────────────────────────────┘└─
549    rcases mem_range.1 hp with ⟨a, rfl⟩,
id            └───────┘   └┘
src    └─────┘└───────┘└─┘  └────────────┘
typ    └─────┘└───────┘└─┘└┘└────────────┘
doc    └─────┘         └─┘  └────────────┘
txt    └─────┘         └─┘  └────────────┘
par    └─────┘         └─┘  └────────────┘
pid                   └─┘  └────────────┘
st   ────────────────────────────────────┘└─
550    by_cases eq : f a = g a,
id                        
src    └───────┘  └─┘   
typ    └───────┘  └─┘ 
doc    └───────┘  └─┘    
txt    └───────┘  └─┘    
par    └───────┘  └─┘    
pid              └─┘    
st   ────────────────────────┘└─
551    { dsimp only [pair_apply], rw eq },
id                   └────────┘      └┘
src      └──────────┘└────────┘  └─┘└┘
typ      └──────────┘└────────┘  └─┘└┘
doc      └──────────┘            └─┘  
txt      └──────────┘            └─┘  
par      └──────────┘            └─┘  
pid           └───┘└┘                
st   ───┘└─────────────────────┘└──────┘└┘
552    { have : volume ((pair f g) ⁻¹' {(f a, g a)}) = 0,
id              └────┘   └──┘      └─┘      
src      └─────┘└────┘  └──┘  └┘└─┘  └┘  └──┘ └┘
typ      └─────┘└────┘  └──┘  └┘└─┘ └┘└──┘ └┘
doc      └─────┘        └──┘  └┘└─┘    └┘  └──┘ └┘
txt      └─────┘              └┘       └┘  └──┘ └┘
par      └─────┘              └┘       └┘  └──┘ └┘
pid      └───┘└┘              └┘       └┘  └──┘ 
st   ──────────────────────────────────────────────────┘└─
553      { refine volume_mono_null (assume a' ha', _) h,
id                └──────────────┘                    
src        └─────┘└──────────────┘       └──────────┘
typ        └─────┘└──────────────┘       └──────────┘
doc        └─────┘                       └──────────┘
txt        └─────┘                       └──────────┘
par        └─────┘                       └──────────┘
pid                                     └──────────┘
st   ─────┘└──────────────────────────────────────────┘└─
554        simp at ha',
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid            └────┘
st   ────────────────┘└─
555        show f a' ≠ g a',
id                    └┘
src        └───┘    
typ        └───┘  └┘
doc        └───┘     
txt        └───┘     
par        └───┘     
pid        └───┘     
st   ─────────────────────┘└─
556        rwa [ha'.1, ha'.2] },
id              └─┘    └─┘
src        └───┘   └──┘   └──┘
typ        └───┘└─┘└──┘└─┘└──┘
doc        └───┘   └──┘   └──┘
txt        └───┘   └──┘   └──┘
par        └───┘   └──┘   └──┘
pid           └┘   └──┘   └─┘
st   ─────────────┘└─────┘└─┘└┘
557      simp [this] }
id             └──┘
src      └────┘    └┘
typ      └────┘└──┘└┘
doc      └────┘    └┘
txt      └────┘    └┘
par      └────┘    └┘
pid              
st   ───────────────┘└─
558  end
st   ──┘
559  
560  lemma integral_map {β} [measure_space β] (f : α →ₛ ennreal) (g : β →ₛ ennreal)(m : α → β)
id                           └───────────┘         └┘ └─────┘        └┘ └─────┘         
src                          └───────────┘           └┘ └─────┘         └┘ └─────┘
typ                          └───────────┘         └┘ └─────┘        └┘ └─────┘         
doc                          └───────────┘           └┘ └─────┘         └┘ └─────┘
561    (eq : ∀a:α, f a = g (m a)) (h : ∀s:set β, is_measurable s → volume s = volume (m ⁻¹' s)) :
id                                 └─┘   └───────────┘    └────┘   └────┘   └─┘ 
src                                      └─┘    └───────────┘     └────┘    └────┘    └─┘
typ                                └─┘   └───────────┘    └────┘   └────┘   └─┘ 
doc                                              └───────────┘                          └─┘
562    f.integral = g.integral :=
id     └───────┘  └───────┘
src     └───────┘   └───────┘
typ    └───────┘  └───────┘
doc     └───────┘    └───────┘
563  have f_eq : (f : α → ennreal) = g ∘ m := funext eq,
id                      └─────┘         └────┘ └┘
src                       └─────┘           └────┘ └┘
typ                     └─────┘         └────┘ └┘
doc                       └─────┘
564  have vol_f : ∀r, volume (f ⁻¹' {r}) = volume (g ⁻¹' {r}),
id                   └────┘   └─┘     └────┘   └─┘ 
src                   └────┘    └─┘      └────┘    └─┘ 
typ                  └────┘   └─┘     └────┘   └─┘ 
doc                             └─┘                  └─┘
565    by { assume r, rw [h, f_eq, preimage_comp], exact measurable_sn _ _ },
id                          └──┘  └───────────┘         └───────────┘
src         └──────┘  └──┘ └┘    └┘└───────────┘  └────┘└───────────┘└───┘
typ         └──────┘  └──┘└┘└──┘└┘└───────────┘  └────┘└───────────┘└───┘
doc         └──────┘  └──┘ └┘    └┘               └────┘             └───┘
txt         └──────┘  └──┘ └┘    └┘               └────┘             └───┘
par         └──────┘  └──┘ └┘    └┘               └────┘             └───┘
pid         └──────┘    └┘ └┘    └┘                                 └──┘
st       └─────────┘└─────┘└────┘└─────────────┘└─────────────────────────┘└┘
566  begin
st   └─────
567    simp [integral, vol_f],
id           └──────┘  └───┘
src    └────┘└──────┘└┘     
typ    └────┘└──────┘└┘└───┘
doc    └────┘└──────┘└┘     
txt    └────┘        └┘     
par    └────┘        └┘     
pid                └┘     
st   ───────────────────────┘└─
568    refine finset.sum_subset _ _,
id            └───────────────┘
src    └─────┘└───────────────┘└──┘
typ    └─────┘└───────────────┘└──┘
doc    └─────┘                 └──┘
txt    └─────┘                 └──┘
par    └─────┘                 └──┘
pid                           └──┘
st   ─────────────────────────────┘└─
569    { simp [finset.subset_iff, f_eq],
id             └───────────────┘  └──┘
src      └────┘└───────────────┘└┘    
typ      └────┘└───────────────┘└┘└──┘
doc      └────┘                 └┘    
txt      └────┘                 └┘    
par      └────┘                 └┘    
pid                           └┘    
st   ───┘└────────────────────────────┘└─
570      rintros r a rfl, exact ⟨_, rfl⟩ },
id                                  └─┘
src      └─────────────┘  └────┘ └─┘└─┘└┘
typ      └─────────────┘  └────┘ └─┘└─┘└┘
doc      └─────────────┘  └────┘ └─┘   └┘
txt      └─────────────┘  └────┘ └─┘   └┘
par      └─────────────┘  └────┘ └─┘   └┘
pid             └──────┘        └─┘   
st   ──────────────────┘└───────────────┘└┘
571    { assume r hrg hrf,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid      └──────────────┘
st   ───────────────────┘└─
572      rw [simple_func.mem_range, not_exists] at hrf,
id           └───────────────────┘  └────────┘
src      └──┘└───────────────────┘└┘└────────┘└──────┘
typ      └──┘└───────────────────┘└┘└────────┘└──────┘
doc      └──┘                     └┘          └──────┘
txt      └──┘                     └┘          └──────┘
par      └──┘                     └┘          └──────┘
pid        └┘                     └┘          └─────┘
st   ────────────────────────────┘└──────────┘└─────┘└─
573      have : f ⁻¹' {r} = ∅ := set.eq_empty_of_subset_empty (assume a, by simpa using hrf a),
id               └─┘         └──────────────────────────┘                           └─┘ 
src      └─────┘ └─┘└─┘└──┘└──────────────────────────┘       └──┘  └──────────┘    
typ      └─────┘└─┘└─┘└──┘└──────────────────────────┘       └──┘  └──────────┘└─┘
doc      └─────┘ └─┘ └─┘  └──┘                                   └──┘  └──────────┘    
txt      └─────┘     └─┘  └──┘                                   └──┘  └──────────┘    
par      └─────┘     └─┘  └──┘                                   └──┘  └──────────┘    
pid      └───┘└┘     └─┘  └──┘                                   └──┘  └───────────┘    
st   ─────────────────────────────────────────────────────────────────────┘└────────────────┘└─
574      simp [(vol_f _).symm, this] }
id              └───┘          └──┘
src      └────┘      └────────┘    └┘
typ      └────┘ └───┘└────────┘└──┘└┘
doc      └────┘      └────────┘    └┘
txt      └────┘      └────────┘    └┘
par      └────┘      └────────┘    └┘
pid                └────────┘    
st   ───────────────────────────────┘└─
575  end
st   ──┘
576  
577  end measure
578  
579  section fin_vol_supp
580  
581  variables [measure_space α] [has_zero β] [has_zero γ]
id              └───────────┘     └──────┘     └──────┘
src             └───────────┘     └──────┘     └──────┘
typ             └───────────┘     └──────┘     └──────┘
doc             └───────────┘
582  
583  open finset ennreal
584  
585  protected def fin_vol_supp (f : α →ₛ β) : Prop := ∀b ≠ 0, volume (f ⁻¹' {b}) < ⊤
id                                    └┘                    └────┘   └─┘     
src                                    └┘                     └────┘    └─┘      
typ                                   └┘                    └────┘   └─┘     
doc                                    └┘                                └─┘
586  
587  lemma fin_vol_supp_map {f : α →ₛ β} {g : β → γ} (hf : f.fin_vol_supp) (hg : g 0 = 0) :
id                                └┘                   └───────────┘           
src                                └┘                       └───────────┘            
typ                               └┘                   └───────────┘           
doc                                └┘
588    (f.map g).fin_vol_supp :=
id      └──┘  └──────────┘
src      └──┘   └──────────┘
typ     └──┘  └──────────┘
doc      └──┘
589  begin
st   └─────
590    assume c hc,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
591    simp only [map_preimage, volume_bUnion_preimage],
id                └──────────┘  └────────────────────┘
src    └─────────┘└──────────┘└┘└────────────────────┘
typ    └─────────┘└──────────┘└┘└────────────────────┘
doc    └─────────┘            └┘                      
txt    └─────────┘            └┘                      
par    └─────────┘            └┘                      
pid        └──┘└┘            └┘                      
st   ─────────────────────────────────────────────────┘└─
592    apply sum_lt_top,
id           └────────┘
src    └────┘└────────┘
typ    └────┘└────────┘
doc    └────┘└────────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────┘└─
593    intro b,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
594    simp only [mem_filter, mem_range, mem_singleton_iff, and_imp, exists_imp_distrib],
id                └────────┘  └───────┘  └───────────────┘  └─────┘  └────────────────┘
src    └─────────┘└────────┘└┘└───────┘└┘└───────────────┘└┘└─────┘└┘└────────────────┘
typ    └─────────┘└────────┘└┘└───────┘└┘└───────────────┘└┘└─────┘└┘└────────────────┘
doc    └─────────┘          └┘         └┘                 └┘       └┘                  
txt    └─────────┘          └┘         └┘                 └┘       └┘                  
par    └─────────┘          └┘         └┘                 └┘       └┘                  
pid        └──┘└┘          └┘         └┘                 └┘       └┘                  
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
595    intros a fab gbc,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
596    apply hf,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
597    intro b0,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid         └─┘
st   ─────────┘└─
598    rw [b0, hg] at gbc, rw gbc at hc,
id         └┘  └┘             └─┘
src    └──┘  └┘  └──────┘  └─┘   └────┘
typ    └──┘└┘└┘└┘└──────┘  └─┘└─┘└────┘
doc    └──┘  └┘  └──────┘  └─┘   └────┘
txt    └──┘  └┘  └──────┘  └─┘   └────┘
par    └──┘  └┘  └──────┘  └─┘   └────┘
pid      └┘  └┘  └─────┘       └────┘
st   ───────┘└──┘└─────┘└────────────┘└─
599    contradiction
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid                 
st   ───────────────┘
600  end
st   └─┘
601  
602  lemma fin_vol_supp_of_fin_vol_supp_map (f : α →ₛ β) {g : β → γ} (h : (f.map g).fin_vol_supp)
id                                                └┘                   └──┘  └──────────┘
src                                                └┘                       └──┘   └──────────┘
typ                                               └┘                   └──┘  └──────────┘
doc                                                └┘                       └──┘
603    (hg : ∀b, g b = 0 → b = 0) : f.fin_vol_supp :=
id                            └───────────┘
src                                └───────────┘
typ                           └───────────┘
604  begin
st   └─────
605    assume b hb,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
606    by_cases b_mem : b ∈ f.range,
id                        └─────┘
src    └───────┘     └─┘ └─────┘
typ    └───────┘     └─┘└─────┘
doc    └───────┘     └─┘  └─────┘
txt    └───────┘     └─┘  
par    └───────┘     └─┘  
pid                 └─┘  
st   ─────────────────────────────┘└─
607    { have gb0 : g b ≠ 0, { assume h, have := hg b h, contradiction },
id                                            └┘  
src      └─────────┘  └┘    └──────┘  └──────┘      └────────────┘
typ      └─────────┘└┘    └──────┘  └──────┘└┘  └────────────┘
doc      └─────────┘   └┘    └──────┘  └──────┘      └────────────┘
txt      └─────────┘   └┘    └──────┘  └──────┘      └────────────┘
par      └─────────┘   └┘    └──────┘  └──────┘      └────────────┘
pid      └──────┘└─┘       └──────┘  └───┘└─┘                   
st   ───┘└────────────────┘└──┘└──────┘└──────────────┘└──────────────┘└┘
608      have : f ⁻¹' {b} ⊆ (f.map g) ⁻¹' {g b},
id                └─┘       └───┘          
src      └─────┘ └─┘ └─┘ └───┘ └┘   └┘ 
typ      └─────┘ └─┘ └─┘ └───┘ └┘   └┘
doc      └─────┘ └─┘ └─┘  └───┘ └┘    └┘ 
txt      └─────┘     └─┘        └┘    └┘ 
par      └─────┘     └─┘        └┘    └┘ 
pid      └───┘└┘     └─┘        └┘    └┘ 
st   ─────────────────────────────────────────┘└─
609        rw [coe_map, @preimage_comp _ _ _ f g, preimage_subset_preimage_iff],
id             └─────┘   └───────────┘          └──────────────────────────┘
src        └──┘└─────┘└┘ └───────────┘└─────┘  └┘└──────────────────────────┘
typ        └──┘└─────┘└┘ └───────────┘└─────┘└┘└──────────────────────────┘
doc        └──┘       └┘              └─────┘  └┘                            
txt        └──┘       └┘              └─────┘  └┘                            
par        └──┘       └┘              └─────┘  └┘                            
pid          └┘       └┘              └─────┘  └┘                            
st   ────────────────┘└────────────────────────┘└────────────────────────────┘└──
610        { simp only [set.mem_preimage, set.mem_singleton, set.singleton_subset_iff] },
id                      └──────────────┘  └───────────────┘  └──────────────────────┘
src          └─────────┘└──────────────┘└┘└───────────────┘└┘└──────────────────────┘└┘
typ          └─────────┘└──────────────┘└┘└───────────────┘└┘└──────────────────────┘└┘
doc          └─────────┘                └┘                 └┘                        └┘
txt          └─────────┘                └┘                 └┘                        └┘
par          └─────────┘                └┘                 └┘                        └┘
pid              └──┘└┘                └┘                 └┘                        
st   ───────┘└────────────────────────────────────────────────────────────────────────┘└┘
611        { rw singleton_subset_iff, rw mem_range at b_mem, exact b_mem },
id              └──────────────────┘     └───────┘                 └───┘
src          └─┘└──────────────────┘  └─┘└───────┘└───────┘  └────┘     
typ          └─┘└──────────────────┘  └─┘└───────┘└───────┘  └────┘└───┘
doc          └─┘                      └─┘         └───────┘  └────┘     
txt          └─┘                      └─┘         └───────┘  └────┘     
par          └─┘                      └─┘         └───────┘  └────┘     
pid                                             └───────┘            
st   ───────┘└─────────────────────┘└─────────────────────┘└────────────┘└┘
612      exact lt_of_le_of_lt (volume_mono this) (h (g b) gb0) },
id             └────────────┘  └─────────┘ └──┘        └─┘
src      └────┘└────────────┘ └─────────┘    └┘     └┘   └┘
typ      └────┘└────────────┘ └─────────┘└──┘└┘  └┘└─┘└┘
doc      └────┘                              └┘     └┘   └┘
txt      └────┘                              └┘     └┘   └┘
par      └────┘                              └┘     └┘   └┘
pid                                         └┘     └┘   
st   ─────────────────────────────────────────────────────────┘└┘
613    { rw ← preimage_eq_empty_iff at b_mem,
id            └───────────────────┘
src      └───┘└───────────────────┘└───────┘
typ      └───┘└───────────────────┘└───────┘
doc      └───┘                     └───────┘
txt      └───┘                     └───────┘
par      └───┘                     └───────┘
pid        └─┘                     └───────┘
st   ──────────────────────────────────────┘└─
614      rw [b_mem, volume_empty],
id           └───┘  └──────────┘
src      └──┘     └┘└──────────┘
typ      └──┘└───┘└┘└──────────┘
doc      └──┘     └┘            
txt      └──┘     └┘            
par      └──┘     └┘            
pid        └┘     └┘            
st   ────────────┘└────────────┘└──
615      exact with_top.zero_lt_top }
id             └──────────────────┘
src      └────┘└──────────────────┘
typ      └────┘└──────────────────┘
doc      └────┘                    
txt      └────┘                    
par      └────┘                    
pid                               
st   ──────────────────────────────┘└─
616  end
st   ──┘
617  
618  lemma fin_vol_supp_pair {f : α →ₛ β} {g : α →ₛ γ} (hf : f.fin_vol_supp) (hg : g.fin_vol_supp) :
id                                 └┘         └┘         └───────────┘        └───────────┘
src                                 └┘           └┘           └───────────┘         └───────────┘
typ                                └┘         └┘         └───────────┘        └───────────┘
doc                                 └┘           └┘
619    (pair f g).fin_vol_supp :=
id      └──┘   └──────────┘
src     └──┘     └──────────┘
typ     └──┘   └──────────┘
doc     └──┘
620  begin
st   └─────
621    rintros ⟨b, c⟩ hbc,
src    └────────────────┘
typ    └────────────────┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid           └─────────┘
st   ───────────────────┘└─
622    rw [pair_preimage_singleton],
id         └─────────────────────┘
src    └──┘└─────────────────────┘
typ    └──┘└─────────────────────┘
doc    └──┘                       
txt    └──┘                       
par    └──┘                       
pid      └┘                       
st   ────────────────────────────┘└──
623    rw [ne.def, prod.eq_iff_fst_eq_snd_eq, not_and_distrib] at hbc,
id         └────┘  └───────────────────────┘  └─────────────┘
src    └──┘└────┘└┘└───────────────────────┘└┘└─────────────┘└──────┘
typ    └──┘└────┘└┘└───────────────────────┘└┘└─────────────┘└──────┘
doc    └──┘      └┘                         └┘               └──────┘
txt    └──┘      └┘                         └┘               └──────┘
par    └──┘      └┘                         └┘               └──────┘
pid      └┘      └┘                         └┘               └─────┘
st   ───────────┘└─────────────────────────┘└───────────────┘└─────┘└─
624    refine or.elim hbc (λ h : b≠0, _) (λ h : c≠0, _),
id            └─────┘ └─┘                     
src    └─────┘└─────┘     └───┘ └────┘  └───┘  └───┘
typ    └─────┘└─────┘└─┘  └───┘└────┘  └───┘└───┘
doc    └─────┘            └───┘  └────┘  └───┘  └───┘
txt    └─────┘            └───┘  └────┘  └───┘  └───┘
par    └─────┘            └───┘  └────┘  └───┘  └───┘
pid                      └───┘  └────┘  └───┘  └───┘
st   ─────────────────────────────────────────────────┘└─
625    { calc _ ≤ volume (f ⁻¹' {b}) : volume_mono (set.inter_subset_left _ _)
id       └──┘     └────┘   └─┘      └─────────┘  └───────────────────┘
src      └──┘     └────┘    └─┘       └─────────┘  └───────────────────┘
typ      └──┘     └────┘   └─┘      └─────────┘  └───────────────────┘
doc      └──┘               └─┘
st   ───┘└─────────────────────────────────────────────────────────────────────
626        ... < ⊤ : hf _ h },
id                  └┘   
src              
typ                 └┘   
st   ─────────────────────┘└─┘
627    { calc _ ≤ volume (g ⁻¹' {c}) : volume_mono (set.inter_subset_right _ _)
id       └──┘     └────┘             └─────────┘  └────────────────────┘
src      └──┘     └────┘               └─────────┘  └────────────────────┘
typ      └──┘     └────┘             └─────────┘  └────────────────────┘
doc      └──┘
st   ───────────────────────────────────────────────────────────────────────────
628        ... < ⊤ : hg _ h },
id                   └┘   
typ                  └┘   
st   ─────────────────────┘└───
629  end
st   ──┘
630  
631  lemma integral_lt_top_of_fin_vol_supp {f : α →ₛ ennreal} (h₁ : ∀ₘ a, f a < ⊤) (h₂ : f.fin_vol_supp) :
id                                               └┘ └─────┘        └┘             └───────────┘
src                                               └┘ └─────┘        └┘                 └───────────┘
typ                                              └┘ └─────┘        └┘             └───────────┘
doc                                               └┘ └─────┘        └┘  
632    integral f < ⊤ :=
id     └──────┘   
src    └──────┘    
typ    └──────┘   
doc    └──────┘
633  begin
st   └─────
634    rw integral, apply sum_lt_top,
id        └──────┘        └────────┘
src    └─┘└──────┘  └────┘└────────┘
typ    └─┘└──────┘  └────┘└────────┘
doc    └─┘└──────┘  └────┘└────────┘
txt    └─┘          └────┘
par    └─┘          └────┘
pid                     
st   ────────────┘└────────────────┘└─
635    intros a ha,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
636    have : f ⁻¹' {⊤} = -{a : α | f a < ⊤}, { ext, simp },
id              └─┘              
src    └─────┘ └─┘└┘└──┘ └─┘       └─┘  └───┘
typ    └─────┘ └─┘└┘└──┘└─┘      └─┘  └───┘
doc    └─────┘ └─┘  └┘   └──┘ └─┘        └─┘  └───┘
txt    └─────┘      └┘   └──┘ └─┘        └─┘  └───┘
par    └─────┘      └┘   └──┘ └─┘        └─┘  └───┘
pid    └───┘└┘      └┘   └──┘ └─┘                 
st   ──────────────────────────────────────┘└──┘└─┘└─────┘└┘
637    have vol_top : volume (f ⁻¹' {⊤}) = 0, { rw [this, volume, ← measure.mem_a_e_iff], exact h₁ },
id                    └────┘                      └──┘  └────┘    └─────────────────┘         └┘
src    └─────────────┘└────┘      └─┘ └┘    └──┘    └┘└────┘└──┘└─────────────────┘  └────┘  
typ    └─────────────┘└────┘     └─┘ └┘    └──┘└──┘└┘└────┘└──┘└─────────────────┘  └────┘└┘
doc    └─────────────┘             └─┘ └┘    └──┘    └┘      └──┘                     └────┘  
txt    └─────────────┘             └─┘ └┘    └──┘    └┘      └──┘                     └────┘  
par    └─────────────┘             └─┘ └┘    └──┘    └┘      └──┘                     └────┘  
pid    └──────────┘└─┘             └─┘       └┘    └┘      └──┘                            
st   ──────────────────────────────────────┘└──┘└──────┘└──────┘└─────────────────────┘└──────────┘└┘
638    by_cases hat : a = ⊤,
id                    
src    └───────┘   └─┘  
typ    └───────┘   └─┘ 
doc    └───────┘   └─┘  
txt    └───────┘   └─┘  
par    └───────┘   └─┘  
pid               └─┘  
st   ─────────────────────┘└─
639    { rw [hat, vol_top, mul_zero], exact with_top.zero_lt_top },
id           └─┘  └─────┘  └──────┘         └──────────────────┘
src      └──┘   └┘       └┘└──────┘  └────┘└──────────────────┘
typ      └──┘└─┘└┘└─────┘└┘└──────┘  └────┘└──────────────────┘
doc      └──┘   └┘       └┘          └────┘                    
txt      └──┘   └┘       └┘          └────┘                    
par      └──┘   └┘       └┘          └────┘                    
pid        └┘   └┘       └┘                                   
st   ───┘└─────┘└───────┘└────────┘└────────────────────────────┘└┘
640    { by_cases haz : a = 0,
id                      
src      └───────┘   └─┘  └┘
typ      └───────┘   └─┘ └┘
doc      └───────┘   └─┘  └┘
txt      └───────┘   └─┘  └┘
par      └───────┘   └─┘  └┘
pid                 └─┘  
st   ───────────────────────┘└─
641      { rw [haz, zero_mul], exact with_top.zero_lt_top },
id             └─┘  └──────┘         └──────────────────┘
src        └──┘   └┘└──────┘  └────┘└──────────────────┘
typ        └──┘└─┘└┘└──────┘  └────┘└──────────────────┘
doc        └──┘   └┘          └────┘                    
txt        └──┘   └┘          └────┘                    
par        └──┘   └┘          └────┘                    
pid          └┘   └┘                                   
st   ─────┘└─────┘└────────┘└────────────────────────────┘└┘
642      apply mul_lt_top,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
643      { rw ennreal.lt_top_iff_ne_top, exact hat },
id            └───────────────────────┘        └─┘
src        └─┘└───────────────────────┘  └────┘   
typ        └─┘└───────────────────────┘  └────┘└─┘
doc        └─┘                           └────┘   
txt        └─┘                           └────┘   
par        └─┘                           └────┘   
pid                                             
st   ─────┘└──────────────────────────┘└──────────┘└┘
644      apply h₂,
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
645      exact haz }
id             └─┘
src      └────┘   
typ      └────┘└─┘
doc      └────┘   
txt      └────┘   
par      └────┘   
pid              
st   ─────────────┘└─
646  end
st   ──┘
647  
648  lemma fin_vol_supp_of_integral_lt_top {f : α →ₛ ennreal} (h : integral f < ⊤) : f.fin_vol_supp :=
id                                               └┘ └─────┘       └──────┘       └───────────┘
src                                               └┘ └─────┘       └──────┘         └───────────┘
typ                                              └┘ └─────┘       └──────┘       └───────────┘
doc                                               └┘ └─────┘       └──────┘
649  begin
st   └─────
650    assume b hb,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
651    rw [integral, sum_lt_top_iff] at h,
id         └──────┘  └────────────┘
src    └──┘└──────┘└┘└────────────┘└────┘
typ    └──┘└──────┘└┘└────────────┘└────┘
doc    └──┘└──────┘└┘└────────────┘└────┘
txt    └──┘        └┘              └────┘
par    └──┘        └┘              └────┘
pid      └┘        └┘              └───┘
st   ─────────────┘└──────────────┘└───┘└─
652    by_cases b_mem : b ∈ f.range,
id                        └─────┘
src    └───────┘     └─┘ └─────┘
typ    └───────┘     └─┘└─────┘
doc    └───────┘     └─┘  └─────┘
txt    └───────┘     └─┘  
par    └───────┘     └─┘  
pid                 └─┘  
st   ─────────────────────────────┘└─
653    { rw ennreal.lt_top_iff_ne_top,
id          └───────────────────────┘
src      └─┘└───────────────────────┘
typ      └─┘└───────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└──────────────────────────┘└─
654      have h : ¬ _ = ⊤ := ennreal.lt_top_iff_ne_top.1 (h b b_mem),
id                         └───────────────────────┘      └───┘
src      └───────┘ └─┘└──┘└───────────────────────┘└─┘        
typ      └───────┘ └─┘└──┘└───────────────────────┘└─┘ └───┘
doc      └───────┘ └─┘  └──┘                         └─┘        
txt      └───────┘ └─┘  └──┘                         └─┘        
par      └───────┘ └─┘  └──┘                         └─┘        
pid      └────┘└─┘ └─┘  └──┘                         └─┘        
st   ──────────────────────────────────────────────────────────────┘└─
655      simp only [mul_eq_top, not_or_distrib, not_and_distrib] at h,
id                  └────────┘  └────────────┘  └─────────────┘
src      └─────────┘└────────┘└┘└────────────┘└┘└─────────────┘└────┘
typ      └─────────┘└────────┘└┘└────────────┘└┘└─────────────┘└────┘
doc      └─────────┘          └┘              └┘               └────┘
txt      └─────────┘          └┘              └┘               └────┘
par      └─────────┘          └┘              └┘               └────┘
pid          └──┘└┘          └┘              └┘               └──┘
st   ───────────────────────────────────────────────────────────────┘└─
656      rcases h with ⟨h, h'⟩,
id              
src      └─────┘ └───────────┘
typ      └─────┘└───────────┘
doc      └─────┘ └───────────┘
txt      └─────┘ └───────────┘
par      └─────┘ └───────────┘
pid             └───────────┘
st   ────────────────────────┘└─
657      refine or.elim h (λh, by contradiction) (λh, h) },
id              └─────┘ 
src      └─────┘└─────┘   └─┘  └───────────┘└┘  └─┘ └┘
typ      └─────┘└─────┘  └─┘  └───────────┘└┘  └─┘ └┘
doc      └─────┘          └─┘  └───────────┘└┘  └─┘ └┘
txt      └─────┘          └─┘  └───────────┘└┘  └─┘ └┘
par      └─────┘          └─┘  └───────────┘└┘  └─┘ └┘
pid                      └─┘  └──────────────┘  └─┘ 
st   ───────────────────────────┘└────────────┘└────────┘└┘
658    { rw ← preimage_eq_empty_iff at b_mem,
id            └───────────────────┘
src      └───┘└───────────────────┘└───────┘
typ      └───┘└───────────────────┘└───────┘
doc      └───┘                     └───────┘
txt      └───┘                     └───────┘
par      └───┘                     └───────┘
pid        └─┘                     └───────┘
st   ──────────────────────────────────────┘└─
659      rw [b_mem, volume_empty],
id           └───┘  └──────────┘
src      └──┘     └┘└──────────┘
typ      └──┘└───┘└┘└──────────┘
doc      └──┘     └┘            
txt      └──┘     └┘            
par      └──┘     └┘            
pid        └┘     └┘            
st   ────────────┘└────────────┘└──
660      exact with_top.zero_lt_top }
id             └──────────────────┘
src      └────┘└──────────────────┘
typ      └────┘└──────────────────┘
doc      └────┘                    
txt      └────┘                    
par      └────┘                    
pid                               
st   ──────────────────────────────┘└─
661  end
st   ──┘
662  
663  /-- A technical lemma dealing with the definition of `integrable` in `l1_space.lean`. -/
664  lemma integral_map_coe_lt_top {f : α →ₛ β} {g : β → nnreal} (h : f.fin_vol_supp) (hg : g 0 = 0) :
id                                       └┘           └────┘       └───────────┘           
src                                       └┘             └────┘        └───────────┘            
typ                                      └┘           └────┘       └───────────┘           
doc                                       └┘             └────┘
665    integral (f.map ((coe : nnreal → ennreal) ∘ g)) < ⊤ :=
id     └──────┘  └──┘   └─┘   └────┘   └─────┘       
src    └──────┘   └──┘   └─┘   └────┘   └─────┘        
typ    └──────┘  └──┘   └─┘   └────┘   └─────┘       
doc    └──────┘   └──┘         └────┘   └─────┘
666  integral_lt_top_of_fin_vol_supp
id   └─────────────────────────────┘
src  └─────────────────────────────┘
typ  └─────────────────────────────┘
667    (by { filter_upwards[], assume a, simp only [mem_set_of_eq, map_apply], exact ennreal.coe_lt_top})
id                                                  └───────────┘  └───────┘         └────────────────┘
src          └──────────────┘  └──────┘  └─────────┘└───────────┘└┘└───────┘  └────┘└────────────────┘
typ          └──────────────┘  └──────┘  └─────────┘└───────────┘└┘└───────┘  └────┘└────────────────┘
doc          └──────────────┘  └──────┘  └─────────┘             └┘           └────┘
txt          └──────────────┘  └──────┘  └─────────┘             └┘           └────┘
par          └──────────────┘  └──────┘  └─────────┘             └┘           └────┘
pid                        └┘  └──────┘      └──┘└┘             └┘                
st        └─────────────────┘└────────┘└────────────────────────────────────┘└────────────────────────┘└┘
668    (by { apply fin_vol_supp_map h, simp only [hg, function.comp_app, ennreal.coe_zero] })
id                 └──────────────┘              └┘  └───────────────┘  └──────────────┘
src          └────┘└──────────────┘   └─────────┘  └┘└───────────────┘└┘└──────────────┘└┘
typ          └────┘└──────────────┘  └─────────┘└┘└┘└───────────────┘└┘└──────────────┘└┘
doc          └────┘                   └─────────┘  └┘                 └┘                └┘
txt          └────┘                   └─────────┘  └┘                 └┘                └┘
par          └────┘                   └─────────┘  └┘                 └┘                └┘
pid                                      └──┘└┘  └┘                 └┘                
st        └─────────────────────────┘└────────────────────────────────────────────────────┘└┘
669  
670  end fin_vol_supp
671  
672  end simple_func
673  
674  section lintegral
675  open simple_func
676  variable [measure_space α]
id             └───────────┘
src            └───────────┘
typ            └───────────┘
doc            └───────────┘
677  
678  /-- The lower Lebesgue integral -/
679  def lintegral (f : α → ennreal) : ennreal :=
id                         └─────┘    └─────┘
src                         └─────┘    └─────┘
typ                        └─────┘    └─────┘
doc                         └─────┘    └─────┘
680  ⨆ (s : α →ₛ ennreal) (hf : f ≥ s), s.integral
id          └┘ └─────┘            └───────┘
src          └┘ └─────┘               └───────┘
typ         └┘ └─────┘            └───────┘
doc          └┘ └─────┘                └───────┘
681  
682  notation `∫⁻` binders `, ` r:(scoped f, lintegral f) := r
id                                           └───────┘
src                                          └───────┘
typ                                          └───────┘
doc                                          └───────┘
683  
684  theorem simple_func.lintegral_eq_integral (f : α →ₛ ennreal) : (∫⁻ a, f a) = f.integral :=
id                                                   └┘ └─────┘     └┘      └───────┘
src                                                   └┘ └─────┘     └┘          └───────┘
typ                                                  └┘ └─────┘     └┘      └───────┘
doc                                                   └┘ └─────┘     └┘           └───────┘
685  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
686    (supr_le $ assume s, supr_le $ assume hs, integral_le_integral _ _ hs)
id      └─────┘            └─────┘          └┘  └──────────────────┘     └┘
src     └─────┘             └─────┘              └──────────────────┘
typ     └─────┘            └─────┘          └┘  └──────────────────┘     └┘
687    (le_supr_of_le f $ le_supr_of_le (le_refl f) $ le_refl _)
id      └───────────┘    └───────────┘  └─────┘     └─────┘
src     └───────────┘     └───────────┘  └─────┘      └─────┘
typ     └───────────┘    └───────────┘  └─────┘     └─────┘
688  
689  lemma lintegral_le_lintegral (f g : α → ennreal) (h : f ≤ g) : (∫⁻ a, f a) ≤ (∫⁻ a, g a) :=
id                                          └─────┘              └┘       └┘   
src                                          └─────┘                └┘          └┘  
typ                                         └─────┘              └┘       └┘   
doc                                          └─────┘                 └┘           └┘  
690  supr_le_supr $ assume s, supr_le $ assume hs, le_supr_of_le (le_trans hs h) (le_refl _)
id   └──────────┘            └─────┘          └┘  └───────────┘  └──────┘ └┘    └─────┘
src  └──────────┘             └─────┘              └───────────┘  └──────┘        └─────┘
typ  └──────────┘            └─────┘          └┘  └───────────┘  └──────┘ └┘    └─────┘
691  
692  lemma lintegral_eq_nnreal (f : α → ennreal) :
id                                     └─────┘
src                                     └─────┘
typ                                    └─────┘
doc                                     └─────┘
693    (∫⁻ a, f a) =
id      └┘     
src     └┘        
typ     └┘     
doc     └┘  
694      (⨆ (s : α →ₛ nnreal) (hf : f ≥ s.map (coe : nnreal → ennreal)), (s.map (coe : nnreal → ennreal)).integral) :=
id               └┘ └────┘          └──┘  └─┘   └────┘   └─────┘    └──┘  └─┘   └────┘   └─────┘  └──────┘
src               └┘ └────┘            └──┘  └─┘   └────┘   └─────┘     └──┘  └─┘   └────┘   └─────┘  └──────┘
typ              └┘ └────┘          └──┘  └─┘   └────┘   └─────┘    └──┘  └─┘   └────┘   └─────┘  └──────┘
doc               └┘ └────┘             └──┘        └────┘   └─────┘     └──┘        └────┘   └─────┘  └──────┘
695  begin
st   └─────
696    let c : nnreal → ennreal := coe,
id             └────┘   └─────┘    └─┘
src    └──────┘└────┘ └─────┘└──┘└─┘
typ    └──────┘└────┘ └─────┘└──┘└─┘
doc    └──────┘└────┘ └─────┘└──┘
txt    └──────┘              └──┘
par    └──────┘              └──┘
pid    └───┘└─┘              └──┘
st   ────────────────────────────────┘└─
697    refine le_antisymm
id            └─────────┘
src    └─────┘└─────────┘
typ    └─────┘└─────────┘
doc    └─────┘           
txt    └─────┘           
par    └─────┘           
pid                     
st   ─────────────────────
698      (supr_le $ assume s, supr_le $ assume hs, _)
src  ───┘               └──┘              └───────
typ  ───┘               └──┘              └───────
doc  ───┘               └──┘              └───────
txt  ───┘               └──┘              └───────
par  ───┘               └──┘              └───────
pid  ───┘               └──┘              └───────
st   ─────────────────────────────────────────────────
699      (supr_le $ assume s, supr_le $ assume hs, le_supr_of_le (s.map c) $ le_supr _ hs),
id                            └─────┘              └───────────┘   └──┘     └─────┘
src  ───┘               └──┘└─────┘       └───┘└───────────┘  └──┘ └┘ └─────┘└─┘  
typ  ───┘               └──┘└─────┘       └───┘└───────────┘  └──┘└┘ └─────┘└─┘  
doc  ───┘               └──┘              └───┘               └──┘ └┘        └─┘  
txt  ───┘               └──┘              └───┘                    └┘        └─┘  
par  ───┘               └──┘              └───┘                    └┘        └─┘  
pid  ───┘               └──┘              └───┘                    └┘        └─┘  
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
700    by_cases ∀ₘ a, s a ≠ ⊤,
id              └┘       
src    └───────┘└┘└┘  
typ    └───────┘└┘└┘ 
doc    └───────┘└┘└┘   
txt    └───────┘  └┘    
par    └───────┘  └┘    
pid              └┘    
st   ───────────────────────┘└─
701    { have : f ≥ (s.map ennreal.to_nnreal).map c :=
id                 └───┘ └───────────────┘      
src      └─────┘  └───┘└───────────────┘└────┘ └───
typ      └─────┘ └───┘└───────────────┘└────┘└───
doc      └─────┘   └───┘└───────────────┘└────┘ └───
txt      └─────┘                         └────┘ └───
par      └─────┘                         └────┘ └───
pid      └───┘└┘                         └────┘ └───
st   ───┘└─────────────────────────────────────────────
702        le_trans (assume a, ennreal.coe_to_nnreal_le_self) hs,
id         └──────┘            └───────────────────────────┘  └┘
src  ─────┘└──────┘       └──┘└───────────────────────────┘└┘
typ  ─────┘└──────┘       └──┘└───────────────────────────┘└┘└┘
doc  ─────┘               └──┘                             └┘
txt  ─────┘               └──┘                             └┘
par  ─────┘               └──┘                             └┘
pid  ─────┘               └──┘                             └┘
st   ──────────────────────────────────────────────────────────┘└─
703      refine le_supr_of_le (s.map ennreal.to_nnreal) (le_supr_of_le this (le_of_eq $ integral_congr _ _ _)),
id                             └───┘ └───────────────┘   └───────────┘ └──┘  └──────┘   └────────────┘
src      └─────┘              └───┘└───────────────┘└┘ └───────────┘     └──────┘ └────────────┘└──────┘
typ      └─────┘              └───┘└───────────────┘└┘ └───────────┘└──┘ └──────┘ └────────────┘└──────┘
doc      └─────┘              └───┘└───────────────┘└┘                                          └──────┘
txt      └─────┘                                    └┘                                          └──────┘
par      └─────┘                                    └┘                                          └──────┘
pid                                                └┘                                          └──────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
704      exact filter.mem_sets_of_superset h (assume a ha, (ennreal.coe_to_nnreal ha).symm) },
id             └─────────────────────────┘                 └───────────────────┘
src      └────┘└─────────────────────────┘        └─────┘ └───────────────────┘  └──────┘
typ      └────┘└─────────────────────────┘       └─────┘ └───────────────────┘  └──────┘
doc      └────┘                                   └─────┘                        └──────┘
txt      └────┘                                   └─────┘                        └──────┘
par      └────┘                                   └─────┘                        └──────┘
pid                                              └─────┘                        └─────┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└┘
705    { have h_vol_s : volume {a : α | s a = ⊤} ≠ 0,
id                      └────┘           
src      └─────────────┘└────┘└──┘ └─┘   └┘ └┘
typ      └─────────────┘└────┘└──┘└─┘  └┘ └┘
doc      └─────────────┘       └──┘ └─┘    └┘ └┘
txt      └─────────────┘       └──┘ └─┘    └┘ └┘
par      └─────────────┘       └──┘ └─┘    └┘ └┘
pid      └──────────┘└─┘       └──┘ └─┘    └┘ 
st   ──────────────────────────────────────────────┘└─
706      { simp [measure_theory.all_ae_iff, set.compl_set_of] at h, assumption },
id               └───────────────────────┘  └──────────────┘
src        └────┘└───────────────────────┘└┘└──────────────┘└────┘  └─────────┘
typ        └────┘└───────────────────────┘└┘└──────────────┘└────┘  └─────────┘
doc        └────┘                         └┘                └────┘  └─────────┘
txt        └────┘                         └┘                └────┘  └─────────┘
par        └────┘                         └┘                └────┘  └─────────┘
pid                                     └┘                └──┘            
st   ─────┘└─────────────────────────────────────────────────────┘└───────────┘└┘
707      let n : ℕ → (α →ₛ nnreal) := λn, restrict (const α (n : nnreal)) (s ⁻¹' {⊤}),
id                     └┘ └────┘         └──────┘  └───┘       └────┘     └─┘ 
src      └──────┘    └┘└────┘└───┘ └─┘└──────┘ └───┘   └─┘└────┘└─┘  └─┘ └┘
typ      └──────┘   └┘└────┘└───┘ └─┘└──────┘ └───┘  └─┘└────┘└─┘ └─┘ └┘
doc      └──────┘    └┘└────┘└───┘ └─┘└──────┘ └───┘   └─┘└────┘└─┘  └─┘  └┘
txt      └──────┘            └───┘ └─┘                 └─┘      └─┘       └┘
par      └──────┘            └───┘ └─┘                 └─┘      └─┘       └┘
pid      └───┘└─┘            └──┘ └─┘                 └─┘      └─┘       └┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
708      have n_le_s : ∀i, (n i).map c ≤ s,
id                                    
src      └────────────┘     └────┘ 
typ      └────────────┘    └────┘
doc      └────────────┘     └────┘  
txt      └────────────┘     └────┘  
par      └────────────┘     └────┘  
pid      └─────────┘└─┘     └────┘  
st   ────────────────────────────────────┘└─
709      { assume i a,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid        └────────┘
st   ─────┘└────────┘└─
710        dsimp [n, c],
id                  
src        └─────┘ └┘ 
typ        └─────┘└┘
doc        └─────┘ └┘ 
txt        └─────┘ └┘ 
par        └─────┘ └┘ 
pid              └┘ 
st   ─────────────────┘└─
711        rw [restrict_apply _ (s.preimage_measurable _)],
id             └────────────┘    └───────────────────┘
src        └──┘└────────────┘└─┘ └───────────────────┘└──┘
typ        └──┘└────────────┘└─┘ └───────────────────┘└──┘
doc        └──┘              └─┘                      └──┘
txt        └──┘              └─┘                      └──┘
par        └──┘              └─┘                      └──┘
pid          └┘              └─┘                      └──┘
st   ───────────────────────────────────────────────────┘└──
712        split_ifs with ha,
src        └───────────────┘
typ        └───────────────┘
doc        └───────────────┘
txt        └───────────────┘
par        └───────────────┘
pid                 └─────┘
st   ──────────────────────┘└─
713        { simp at ha, exact ha.symm ▸ le_top },
id                             └─────┘  └────┘
src          └────────┘  └────┘└─────┘└────┘
typ          └────────┘  └────┘└─────┘└────┘
doc          └────────┘  └────┘              
txt          └────────┘  └────┘              
par          └────────┘  └────┘              
pid              └───┘                     
st   ───────┘└────────┘└───────────────────────┘└┘
714        { exact zero_le _ } },
id                 └─────┘
src          └────┘└─────┘└─┘
typ          └────┘└─────┘└─┘
doc          └────┘       └─┘
txt          └────┘       └─┘
par          └────┘       └─┘
pid                      └┘
st   ───────────────────────┘└──┘
715      have approx_s : ∀ (i : ℕ), ↑i * volume {a : α | s a = ⊤} ≤ integral (map c (n i)),
id                                      └────┘                  └──────┘  └─┘   
src      └──────────────┘ └────┘    └────┘└──┘ └─┘    └┘ └──────┘ └─┘    └┘
typ      └──────────────┘ └────┘    └────┘└──┘└─┘   └┘ └──────┘ └─┘  └┘
doc      └──────────────┘ └────┘            └──┘ └─┘    └┘ └──────┘ └─┘    └┘
txt      └──────────────┘ └────┘            └──┘ └─┘    └┘                 └┘
par      └──────────────┘ └────┘            └──┘ └─┘    └┘                 └┘
pid      └───────────┘└─┘ └────┘            └──┘ └─┘    └┘                 └┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
716      { assume i,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────┘└──────┘└─
717        have : {a : α | s a = ⊤} = s ⁻¹' {⊤}, { ext a, simp },
id                                       
src        └─────┘└──┘ └─┘    └┘          └───┘  └───┘
typ        └─────┘└──┘└─┘    └┘         └───┘  └───┘
doc        └─────┘ └──┘ └─┘    └┘           └───┘  └───┘
txt        └─────┘ └──┘ └─┘    └┘           └───┘  └───┘
par        └─────┘ └──┘ └─┘    └┘           └───┘  └───┘
pid        └───┘└┘ └──┘ └─┘    └┘              └┘      
st   ─────────────────────────────────────────┘└──┘└───┘└─────┘└┘
718        rw [this, ← restrict_const_integral _ _ (s.preimage_measurable _)],
id             └──┘    └─────────────────────┘      └───────────────────┘
src        └──┘    └──┘└─────────────────────┘└───┘ └───────────────────┘└──┘
typ        └──┘└──┘└──┘└─────────────────────┘└───┘ └───────────────────┘└──┘
doc        └──┘    └──┘                       └───┘                      └──┘
txt        └──┘    └──┘                       └───┘                      └──┘
par        └──┘    └──┘                       └───┘                      └──┘
pid          └┘    └──┘                       └───┘                      └──┘
st   ─────────────┘└───────────────────────────────────────────────────────┘└──
719        { refine integral_le_integral _ _ (assume a, le_of_eq _),
id                  └──────────────────┘                └──────┘
src          └─────┘└──────────────────┘└───┘       └──┘└──────┘└─┘
typ          └─────┘└──────────────────┘└───┘       └──┘└──────┘└─┘
doc          └─────┘                    └───┘       └──┘        └─┘
txt          └─────┘                    └───┘       └──┘        └─┘
par          └─────┘                    └───┘       └──┘        └─┘
pid                                    └───┘       └──┘        └─┘
st   ─────────────────────────────────────────────────────────────┘└─
720          simp [n, c, restrict_apply, s.preimage_measurable],
id                     └────────────┘
src          └────┘ └┘ └┘└────────────┘└┘                     
typ          └────┘└┘└┘└────────────┘└┘└───────────────────┘
doc          └────┘ └┘ └┘              └┘                     
txt          └────┘ └┘ └┘              └┘                     
par          └────┘ └┘ └┘              └┘                     
pid               └┘ └┘              └┘                     
st   ─────────────────────────────────────────────────────────┘└─
721          split_ifs; simp [ennreal.coe_nat] },
id                            └─────────────┘
src          └───────┘  └────┘└─────────────┘└┘
typ          └───────┘  └────┘└─────────────┘└┘
doc          └───────┘  └────┘               └┘
txt          └───────┘  └────┘               └┘
par          └───────┘  └────┘               └┘
pid                                        
st   ─────────────────────────────────────────┘└──
722       },
st   ──────┘
723      calc s.integral ≤ ⊤ : le_top
id       └──┘ └────────┘       └────┘
src      └──┘ └────────┘       └────┘
typ      └──┘ └────────┘       └────┘
doc      └──┘ └────────┘
st   ─────────────────────────────────
724        ... = (⨆i:ℕ, (i : ennreal) * volume {a | s a = ⊤}) :
id                                      └────┘     
src                                     └────┘
typ                                     └────┘     
st   ───────────────────────────────────────────────────────────
725          by rw [← ennreal.supr_mul, ennreal.supr_coe_nat, ennreal.top_mul, if_neg h_vol_s]
id                    └──────────────┘  └──────────────────┘  └─────────────┘  └────┘ └─────┘
src             └────┘└──────────────┘└┘└──────────────────┘└┘└─────────────┘└┘└────┘       └─
typ             └────┘└──────────────┘└┘└──────────────────┘└┘└─────────────┘└┘└────┘└─────┘└─
doc             └────┘                └┘                    └┘               └┘             └─
txt             └────┘                └┘                    └┘               └┘             └─
par             └────┘                └┘                    └┘               └┘             └─
pid               └──┘                └┘                    └┘               └┘             
st   ─────────┘└─────────────────────┘└────────────────────┘└───────────────┘└──────────────┘
726        ... ≤ (⨆i, ((n i).map c).integral) : supr_le_supr approx_s
id                              └──────┘     └──────────┘ └──────┘
src  ─────┘                      └──────┘     └──────────┘
typ  ─────┘                     └──────┘     └──────────┘ └──────┘
doc  ─────┘                      └──────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└──────────────────────────────────────────────────────────
727        ... ≤ ⨆ (s : α →ₛ nnreal) (hf : f ≥ s.map c), (s.map c).integral :
id                           └────┘            └──┘              └──────┘
src                          └────┘             └──┘              └──────┘
typ                          └────┘            └──┘              └──────┘
doc                          └────┘             └──┘              └──────┘
st   ─────────────────────────────────────────────────────────────────────────
728          have ∀i, ((n i).map c : α → ennreal) ≤ f := assume i, le_trans (n_le_s i) hs,
id                                     └─────┘                 └──────┘  └────┘    └┘
src                                      └─────┘                   └──────┘
typ                                    └─────┘                 └──────┘  └────┘    └┘
doc                                      └─────┘
st   ──────────────────────────────────────────────────────────────────────────────────────
729          (supr_le $ assume i, le_supr_of_le (n i) (le_supr (λh, ((n i).map c).integral) (this i))) }
id            └─────┘            └───────────┘        └─────┘          └─┘   └──────┘
src           └─────┘             └───────────┘        └─────┘            └─┘    └──────┘
typ           └─────┘            └───────────┘        └─────┘          └─┘   └──────┘
doc                                                                       └─┘    └──────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└──
730  end
st   ──┘
731  
732  /-- Monotone convergence theorem -- somtimes called Beppo-Levi convergence.
733  
734  See `lintegral_supr_directed` for a more general form. -/
735  theorem lintegral_supr
736    {f : ℕ → α → ennreal} (hf : ∀n, measurable (f n)) (h_mono : monotone f) :
id                └─────┘           └────────┘                └──────┘ 
src                └─────┘            └────────┘                  └──────┘
typ               └─────┘           └────────┘                └──────┘ 
doc                 └─────┘            └────────┘                  └──────┘
737    (∫⁻ a, ⨆n, f n a) = (⨆n, ∫⁻ a, f n a) :=
id      └┘          └┘    
src     └┘                └┘  
typ     └┘          └┘    
doc     └┘                 └┘  
738  let c : nnreal → ennreal := coe in
id           └────┘  └─────┘    └─┘
src          └────┘   └─────┘    └─┘
typ          └────┘  └─────┘    └─┘
doc          └────┘   └─────┘
739  let F (a:α) := ⨆n, f n a in
id                   
src                  
typ                  
doc                  
740  have hF : measurable F := measurable.supr hf,
id             └────────┘     └─────────────┘ └┘
src            └────────┘      └─────────────┘
typ            └────────┘     └─────────────┘ └┘
doc            └────────┘
741  show (∫⁻ a, F a) = (⨆n, ∫⁻ a, f n a),
id         └┘        └┘    
src        └┘            └┘  
typ        └┘        └┘    
doc        └┘             └┘  
742  begin
st   └─────
743    refine le_antisymm _ _,
id            └─────────┘
src    └─────┘└─────────┘└──┘
typ    └─────┘└─────────┘└──┘
doc    └─────┘           └──┘
txt    └─────┘           └──┘
par    └─────┘           └──┘
pid                     └──┘
st   ───────────────────────┘└─
744    { rw [lintegral_eq_nnreal],
id           └─────────────────┘
src      └──┘└─────────────────┘
typ      └──┘└─────────────────┘
doc      └──┘                   
txt      └──┘                   
par      └──┘                   
pid        └┘                   
st   ───┘└─────────────────────┘└──
745      refine supr_le (assume s, supr_le (assume hsf, _)),
id                                 └─────┘
src      └─────┘              └──┘└─────┘       └───────┘
typ      └─────┘              └──┘└─────┘       └───────┘
doc      └─────┘              └──┘              └───────┘
txt      └─────┘              └──┘              └───────┘
par      └─────┘              └──┘              └───────┘
pid                          └──┘              └───────┘
st   ─────────────────────────────────────────────────────┘└─
746      refine ennreal.le_of_forall_lt_one_mul_lt (assume a ha, _),
id              └────────────────────────────────┘
src      └─────┘└────────────────────────────────┘       └───────┘
typ      └─────┘└────────────────────────────────┘       └───────┘
doc      └─────┘                                         └───────┘
txt      └─────┘                                         └───────┘
par      └─────┘                                         └───────┘
pid                                                     └───────┘
st   ─────────────────────────────────────────────────────────────┘└─
747      rcases ennreal.lt_iff_exists_coe.1 ha with ⟨r, rfl, ha⟩,
id              └───────────────────────┘   └┘
src      └─────┘└───────────────────────┘└─┘  └────────────────┘
typ      └─────┘└───────────────────────┘└─┘└┘└────────────────┘
doc      └─────┘                         └─┘  └────────────────┘
txt      └─────┘                         └─┘  └────────────────┘
par      └─────┘                         └─┘  └────────────────┘
pid                                     └─┘  └────────────────┘
st   ──────────────────────────────────────────────────────────┘└─
748      have ha : r < 1 := ennreal.coe_lt_coe.1 ha,
id                        └────────────────┘   └┘
src      └────────┘ └────┘└────────────────┘└─┘
typ      └────────┘└────┘└────────────────┘└─┘└┘
doc      └────────┘  └────┘                  └─┘
txt      └────────┘  └────┘                  └─┘
par      └────────┘  └────┘                  └─┘
pid      └─────┘└─┘  └───┘                  └─┘
st   ─────────────────────────────────────────────┘└─
749      let rs := s.map (λa, r * a),
id                 └───┘       
src      └────────┘└───┘  └─┘  
typ      └────────┘└───┘  └─┘ 
doc      └────────┘└───┘  └─┘   
txt      └────────┘       └─┘   
par      └────────┘       └─┘   
pid      └────┘└─┘       └─┘   
st   ──────────────────────────────┘└─
750      have eq_rs : (const α r : α →ₛ ennreal) * map c s = rs.map c,
id                     └───┘       └┘ └─────┘    └─┘     └────┘ 
src      └───────────┘ └───┘  └─┘ └┘└─────┘└┘ └─┘  └────┘
typ      └───────────┘ └───┘└─┘ └┘└─────┘└┘ └─┘ └────┘
doc      └───────────┘ └───┘  └─┘ └┘└─────┘└┘ └─┘   └────┘
txt      └───────────┘        └─┘          └┘             
par      └───────────┘        └─┘          └┘             
pid      └────────┘└─┘        └─┘          └┘             
st   ───────────────────────────────────────────────────────────────┘└─
751      { ext1 a, exact ennreal.coe_mul.symm },
id                       └──────────────────┘
src        └────┘  └────┘└──────────────────┘
typ        └────┘  └────┘└──────────────────┘
doc        └────┘  └────┘                    
txt        └────┘  └────┘                    
par        └────┘  └────┘                    
pid            └┘                           
st   ─────┘└────┘└───────────────────────────┘└┘
752      have eq : ∀p, (rs.map c) ⁻¹' {p} = (⋃n, (rs.map c) ⁻¹' {p} ∩ {a | p ≤ f n a}),
id                                └─┘           └────┘                  
src      └────────┘          └┘└─┘ └─┘   └────┘ └┘   └─┘└──┘    └┘
typ      └────────┘          └┘└─┘ └─┘   └────┘└┘   └─┘└──┘   └┘
doc      └────────┘          └┘└─┘ └─┘   └────┘ └┘    └─┘  └──┘     └┘
txt      └────────┘          └┘    └─┘            └┘    └─┘  └──┘     └┘
par      └────────┘          └┘    └─┘            └┘    └─┘  └──┘     └┘
pid      └─────┘└─┘          └┘    └─┘            └┘    └─┘  └──┘     └┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
753      { assume p,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────┘└──────┘└─
754        rw [← inter_Union, ← inter_univ ((map c rs) ⁻¹' {p})] {occs := occurrences.pos [1]},
id               └─────────┘    └────────┘   └─┘  └┘                    └─────────────┘  
src        └────┘└─────────┘└──┘└────────┘  └─┘   └┘   └───┘ └──────┘└─────────────┘
typ        └────┘└─────────┘└──┘└────────┘  └─┘└┘└┘   └───┘ └──────┘└─────────────┘
doc        └────┘           └──┘            └─┘   └┘    └───┘ └──────┘                 
txt        └────┘           └──┘                  └┘    └───┘ └──────┘                 
par        └────┘           └──┘                  └┘    └───┘ └──────┘                 
pid          └──┘           └──┘                  └┘    └──┘ └──────┘                 
st   ──────────────────────┘└─────────────────────────────────┘└────────────────────────────┘└─
755        refine set.ext (assume x, and_congr_right $ assume hx, (true_iff _).2 _),
id                └─────┘            └─────────────┘               └──────┘
src        └─────┘└─────┘       └──┘└─────────────┘       └───┘ └──────┘└──────┘
typ        └─────┘└─────┘       └──┘└─────────────┘       └───┘ └──────┘└──────┘
doc        └─────┘              └──┘                      └───┘         └──────┘
txt        └─────┘              └──┘                      └───┘         └──────┘
par        └─────┘              └──┘                      └───┘         └──────┘
pid                            └──┘                      └───┘         └──────┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
756        by_cases p_eq : p = 0, { simp [p_eq] },
id                                       └──┘
src        └───────┘    └─┘  └┘    └────┘    └┘
typ        └───────┘    └─┘ └┘    └────┘└──┘└┘
doc        └───────┘    └─┘  └┘    └────┘    └┘
txt        └───────┘    └─┘  └┘    └────┘    └┘
par        └───────┘    └─┘  └┘    └────┘    └┘
pid                    └─┘              
st   ──────────────────────────┘└──┘└──────────┘└┘
757        simp at hx, subst hx,
id                           └┘
src        └────────┘  └────┘
typ        └────────┘  └────┘└┘
doc        └────────┘  └────┘
txt        └────────┘  └────┘
par        └────────┘  └────┘
pid            └───┘       
st   ───────────────┘└────────┘└─
758        have : r * s x ≠ 0, { rwa [(≠), ← ennreal.coe_eq_zero] },
id                                      └─────────────────┘
src        └─────┘    └┘    └───┘└────┘└─────────────────┘└┘
typ        └─────┘ └┘    └───┘└────┘└─────────────────┘└┘
doc        └─────┘     └┘    └───┘ └────┘                   └┘
txt        └─────┘     └┘    └───┘ └────┘                   └┘
par        └─────┘     └┘    └───┘ └────┘                   └┘
pid        └───┘└┘            └┘ └────┘                   
st   ───────────────────────┘└──┘└──────┘└─────────────────────┘└┘
759        have : s x ≠ 0, { refine mt _ this, assume h, rw [h, mul_zero] },
id                                └┘   └──┘                  └──────┘
src        └─────┘   └┘    └─────┘└┘└─┘      └──────┘  └──┘ └┘└──────┘└┘
typ        └─────┘ └┘    └─────┘└┘└─┘└──┘  └──────┘  └──┘└┘└──────┘└┘
doc        └─────┘   └┘    └─────┘  └─┘      └──────┘  └──┘ └┘        └┘
txt        └─────┘   └┘    └─────┘  └─┘      └──────┘  └──┘ └┘        └┘
par        └─────┘   └┘    └─────┘  └─┘      └──────┘  └──┘ └┘        └┘
pid        └───┘└┘               └─┘      └──────┘    └┘ └┘        
st   ───────────────────┘└──┘└──────────────┘└────────┘└─────┘└────────┘└┘
760        have : (rs.map c) x < ⨆ (n : ℕ), f n x,
id                 └────┘                   
src        └─────┘ └────┘ └┘  └────┘   
typ        └─────┘ └────┘└┘  └────┘  
doc        └─────┘ └────┘ └┘  └────┘   
txt        └─────┘        └┘   └────┘    
par        └─────┘        └┘   └────┘    
pid        └───┘└┘        └┘   └────┘    
st   ───────────────────────────────────────────┘└─
761        { refine lt_of_lt_of_le (ennreal.coe_lt_coe.2 (_)) (hsf x),
id                  └────────────┘  └────────────────┘         └─┘ 
src          └─────┘└────────────┘ └────────────────┘└─┘ └──┘     
typ          └─────┘└────────────┘ └────────────────┘└─┘ └──┘ └─┘
doc          └─────┘                                 └─┘ └──┘     
txt          └─────┘                                 └─┘ └──┘     
par          └─────┘                                 └─┘ └──┘     
pid                                                 └─┘ └──┘     
st   ───────┘└──────────────────────────────────────────────────────┘└─
762          suffices : r * s x < 1 * s x, simpa [rs],
id                                             └┘
src          └─────────┘     └─┘     └─────┘  
typ          └─────────┘    └─┘   └─────┘└┘
doc          └─────────┘     └─┘     └─────┘  
txt          └─────────┘     └─┘     └─────┘  
par          └─────────┘     └─┘     └─────┘  
pid          └───────┘└┘     └─┘            
st   ───────────────────────────────────┘└──────────┘└─
763          exact mul_lt_mul_of_pos_right ha (zero_lt_iff_ne_zero.2 this) },
id                 └─────────────────────┘ └┘  └─────────────────┘   └──┘
src          └────┘└─────────────────────┘   └─────────────────┘└─┘    └┘
typ          └────┘└─────────────────────┘└┘ └─────────────────┘└─┘└──┘└┘
doc          └────┘                                             └─┘    └┘
txt          └────┘                                             └─┘    └┘
par          └────┘                                             └─┘    └┘
pid                                                            └─┘    
st   ─────────────────────────────────────────────────────────────────────┘└┘
764        rcases lt_supr_iff.1 this with ⟨i, hi⟩,
id                └─────────┘   └──┘
src        └─────┘└─────────┘└─┘    └───────────┘
typ        └─────┘└─────────┘└─┘└──┘└───────────┘
doc        └─────┘           └─┘    └───────────┘
txt        └─────┘           └─┘    └───────────┘
par        └─────┘           └─┘    └───────────┘
pid                         └─┘    └───────────┘
st   ───────────────────────────────────────────┘└─
765        exact mem_Union.2 ⟨i, le_of_lt hi⟩ },
id               └───────┘      └──────┘ └┘
src        └────┘└───────┘└─┘  └┘└──────┘  └┘
typ        └────┘└───────┘└─┘ └┘└──────┘└┘└┘
doc        └────┘         └─┘  └┘          └┘
txt        └────┘         └─┘  └┘          └┘
par        └────┘         └─┘  └┘          └┘
pid                      └─┘  └┘          
st   ────────────────────────────────────────┘└┘
766      have mono : ∀r:ennreal, monotone (λn, (rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a}),
id                      └─────┘  └──────┘       └────┘                    
src      └──────────┘ └┘└─────┘ └──────┘  └─┘ └────┘ └┘   └─┘ └──┘     └┘
typ      └──────────┘ └┘└─────┘ └──────┘  └─┘ └────┘└┘   └─┘ └──┘    └┘
doc      └──────────┘ └┘└─────┘ └──────┘  └─┘ └────┘ └┘    └─┘  └──┘     └┘
txt      └──────────┘ └┘                  └─┘        └┘    └─┘  └──┘     └┘
par      └──────────┘ └┘                  └─┘        └┘    └─┘  └──┘     └┘
pid      └───────┘└─┘ └┘                  └─┘        └┘    └─┘  └──┘     └┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
767      { assume r i j h,
src        └────────────┘
typ        └────────────┘
doc        └────────────┘
txt        └────────────┘
par        └────────────┘
pid        └────────────┘
st   ─────┘└────────────┘└─
768        refine inter_subset_inter (subset.refl _) _,
id                └────────────────┘  └─────────┘
src        └─────┘└────────────────┘ └─────────┘└───┘
typ        └─────┘└────────────────┘ └─────────┘└───┘
doc        └─────┘                              └───┘
txt        └─────┘                              └───┘
par        └─────┘                              └───┘
pid                                            └───┘
st   ────────────────────────────────────────────────┘└─
769        assume x hx, exact le_trans hx (h_mono h x) },
id                            └──────┘ └┘  └────┘  
src        └─────────┘  └────┘└──────┘           └┘
typ        └─────────┘  └────┘└──────┘└┘ └────┘└┘
doc        └─────────┘  └────┘                   └┘
txt        └─────────┘  └────┘                   └┘
par        └─────────┘  └────┘                   └┘
pid        └─────────┘                          
st   ────────────────┘└───────────────────────────────┘└┘
770      have h_meas : ∀n, is_measurable {a : α | ⇑(map c rs) a ≤ f n a} :=
id                         └───────────┘         └─┘  └┘      
src      └────────────┘  └───────────┘└──┘ └─┘ └─┘   └┘     └────
typ      └────────────┘  └───────────┘└──┘└─┘ └─┘└┘└┘    └────
doc      └────────────┘  └───────────┘ └──┘ └─┘  └─┘   └┘     └────
txt      └────────────┘                └──┘ └─┘        └┘     └────
par      └────────────┘                └──┘ └─┘        └┘     └────
pid      └─────────┘└─┘                └──┘ └─┘        └┘     └───
st   ───────────────────────────────────────────────────────────────────────
771        assume n, is_measurable_le (simple_func.measurable _) (hf n),
id                   └──────────────┘  └────────────────────┘     └┘
src  ─────┘      └──┘└──────────────┘ └────────────────────┘└──┘    
typ  ─────┘      └──┘└──────────────┘ └────────────────────┘└──┘ └┘ 
doc  ─────┘      └──┘                 └────────────────────┘└──┘    
txt  ─────┘      └──┘                                       └──┘    
par  ─────┘      └──┘                                       └──┘    
pid  ─────┘      └──┘                                       └──┘    
st   ─────────────────────────────────────────────────────────────────┘└─
772      calc (r:ennreal) * integral (s.map c) = (rs.map c).range.sum (λr, r * volume ((rs.map c) ⁻¹' {r})) :
id       └──┘   └─────┘    └──────┘  └───┘                                   └────┘   └────┘ 
src      └──┘    └─────┘    └──────┘  └───┘                                    └────┘   └────┘
typ      └──┘   └─────┘    └──────┘  └───┘                                   └────┘   └────┘ 
doc      └──┘    └─────┘    └──────┘  └───┘                                             └────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────
773          by rw [← const_mul_integral, integral, eq_rs]
id                    └────────────────┘  └──────┘  └───┘
src             └────┘└────────────────┘└┘└──────┘└┘     └─
typ             └────┘└────────────────┘└┘└──────┘└┘└───┘└─
doc             └────┘                  └┘└──────┘└┘     └─
txt             └────┘                  └┘        └┘     └─
par             └────┘                  └┘        └┘     └─
pid               └──┘                  └┘        └┘     
st   ─────────┘└───────────────────────┘└────────┘└─────┘
774        ... ≤ (rs.map c).range.sum (λr, r * volume (⋃n, (rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a})) :
id                                                                                    
src  ─────┘
typ  ─────┘                                                                           
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└────────────────────────────────────────────────────────────────────────────────────────
775          le_of_eq (finset.sum_congr rfl $ assume x hx, by rw ← eq)
id                                                    └┘          └┘
src                                                           └───┘└┘
typ                                                   └┘     └───┘└┘
doc                                                           └───┘
txt                                                           └───┘
par                                                           └───┘
pid                                                             └─┘
st   ───────────────────────────────────────────────────────┘└──────┘└─
776        ... ≤ (rs.map c).range.sum (λr, (⨆n, r * volume ((rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a}))) :
id                                                                              
typ                                                                             
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
777          le_of_eq (finset.sum_congr rfl $ assume x hx,
id           └──────┘  └──────────────┘ └─┘           └┘
src          └──────┘  └──────────────┘ └─┘
typ          └──────┘  └──────────────┘ └─┘           └┘
st   ──────────────────────────────────────────────────────
778            begin
st   ─────────┘└─────
779              rw [volume, measure_Union_eq_supr_nat _ (mono x), ennreal.mul_supr],
id                   └────┘  └───────────────────────┘    └──┘    └──────────────┘
src              └──┘└────┘└┘└───────────────────────┘└─┘      └─┘└──────────────┘
typ              └──┘└────┘└┘└───────────────────────┘└─┘ └──┘└─┘└──────────────┘
doc              └──┘      └┘                         └─┘      └─┘                
txt              └──┘      └┘                         └─┘      └─┘                
par              └──┘      └┘                         └─┘      └─┘                
pid                └┘      └┘                         └─┘      └─┘                
st   ─────────────────────┘└────────────────────────────────────┘└────────────────┘└──
780              { assume i,
src                └──────┘
typ                └──────┘
doc                └──────┘
txt                └──────┘
par                └──────┘
pid                └──────┘
st   ─────────────────────┘└─
781                refine is_measurable.inter ((rs.map c).preimage_measurable _) _,
id                        └─────────────────┘   └────┘ 
src                └─────┘└─────────────────┘  └────┘ └────────────────────────┘
typ                └─────┘└─────────────────┘  └────┘└────────────────────────┘
doc                └─────┘                     └────┘ └────────────────────────┘
txt                └─────┘                            └────────────────────────┘
par                └─────┘                            └────────────────────────┘
pid                                                  └────────────────────────┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
782                refine (hf i).preimage _,
id                         └┘ 
src                └─────┘    └──────────┘
typ                └─────┘ └┘└──────────┘
doc                └─────┘    └──────────┘
txt                └─────┘    └──────────┘
par                └─────┘    └──────────┘
pid                          └──────────┘
st   ─────────────────────────────────────┘
783                exact is_measurable_of_is_closed (is_closed_ge' _) }
st                                                                    └┘
784            end)
st             └─┘
785        ... ≤ ⨆n, (rs.map c).range.sum (λr, r * volume ((rs.map c) ⁻¹' {r} ∩ {a | r ≤ f n a})) :
id                                                                             
typ                                                                            
786          begin
787            refine le_of_eq _,
788            rw [ennreal.finset_sum_supr_nat],
789            assume p i j h,
790            exact canonically_ordered_semiring.mul_le_mul (le_refl _) (volume_mono $ mono p h)
id                                                                                           
typ                                                                                          
791          end
st           └─┘
792        ... ≤ (⨆n:ℕ, ((rs.map c).restrict {a | (rs.map c) a ≤ f n a}).integral) :
id                                            
typ                                           
793        begin
794          refine supr_le_supr (assume n, _),
id                                       
typ                                      
795          rw [restrict_integral _ _ (h_meas n)],
id                                             
typ                                            
796          { refine le_of_eq (finset.sum_congr rfl $ assume r hr, _),
id                                                            
typ                                                           
797            congr' 2,
798            ext a,
799            refine and_congr_right _,
800            simp {contextual := tt} }
id                                 └┘
src                                └┘
typ                                └┘
st                                     └┘
801        end
st         └─┘
802        ... ≤ (⨆n, ∫⁻ a, f n a) :
id                      
typ                     
803        begin
804          refine supr_le_supr (assume n, _),
id                                       
typ                                      
805          rw [← simple_func.lintegral_eq_integral],
806          refine lintegral_le_lintegral _ _ (assume a, _),
id                                                     
typ                                                    
807          dsimp,
808          rw [restrict_apply],
809          split_ifs; simp, simpa using h,
810          exact h_meas n
id                        
typ                       
811        end },
st         └─┘ └┘
812    { exact supr_le (assume n, lintegral_le_lintegral _ _ $ assume a, le_supr _ n) }
id                                                                   
typ                                                                  
st                                                                                    └─
813  end
st   ──┘
814  
815  lemma lintegral_eq_supr_eapprox_integral {f : α → ennreal} (hf : measurable f) :
id                                                    └─────┘                   
src                                                    └─────┘
typ                                                   └─────┘                   
doc                                                    └─────┘
816    (∫⁻ a, f a) = (⨆n, (eapprox f n).integral) :=
id                              
typ                             
817  calc (∫⁻ a, f a) = (∫⁻ a, ⨆n, (eapprox f n : α → ennreal) a) :
id                                            └───┘   
src                                                   └───┘ 
typ                                           └───┘   
doc                                                   └───┘ 
818     by congr; ext a; rw [supr_eapprox_apply f hf]
id                                              
typ                                             
st                                                  
819   ... = (⨆n, ∫⁻ a, (eapprox f n : α → ennreal) a) :
id                                   └─────┘  
src                                       └─────┘
typ                                  └─────┘  
doc                                       └─────┘
820   begin
821     rw [lintegral_supr],
822     { assume n, exact (eapprox f n).measurable },
id                                  
typ                                 
st                                                 └┘
823     { assume i j h, exact (monotone_eapprox f h) }
id                                              
typ                                             
st                                                   └┘
824   end
st    └─┘
825   ... = (⨆n, (eapprox f n).integral) : by congr; ext n; rw [(eapprox f n).lintegral_eq_integral]
id                                                                     
typ                                                                    
st                                                                                                 
826  
827  lemma lintegral_add {f g : α → ennreal} (hf : measurable f) (hg : measurable g) :
id                                 └─────┘                                      
src                                 └─────┘
typ                                └─────┘                                      
doc                                 └─────┘
828    (∫⁻ a, f a + g a) = (∫⁻ a, f a) + (∫⁻ a, g a) :=
id                                      
typ                                     
829  calc (∫⁻ a, f a + g a) =
id                     
typ                    
830      (∫⁻ a, (⨆n, (eapprox f n : α → ennreal) a) + (⨆n, (eapprox g n : α → ennreal) a)) :
id                                  └───┘                           └────┘   
src                                      └───┘                               └────┘
typ                                 └───┘                           └────┘   
doc                                      └───┘                               └────┘
831      by congr; funext a; rw [supr_eapprox_apply f hf, supr_eapprox_apply g hg]
id                                                                          
typ                                                                         
st                                                                               
832    ... = (∫⁻ a, (⨆n, (eapprox f n + eapprox g n : α → ennreal) a)) :
id                                                 └─────┘  
src                                                       └─────┘
typ                                                └─────┘  
doc                                                       └─────┘
833    begin
834      congr, funext a,
835      rw [ennreal.supr_add_supr_of_monotone], { refl },
st                                                      └┘
836      { assume i j h, exact monotone_eapprox _ h a },
id                                                  
typ                                                 
st                                                    └┘
837      { assume i j h, exact monotone_eapprox _ h a },
id                                                  
typ                                                 
st                                                    └┘
838    end
st     └─┘
839    ... = (⨆n, (eapprox f n).integral + (eapprox g n).integral) :
id                                                
typ                                               
840    begin
841      rw [lintegral_supr],
842      { congr, funext n, rw [← simple_func.add_integral, ← simple_func.lintegral_eq_integral], refl },
st                                                                                                     └┘
843      { assume n, exact measurable.add (eapprox f n).measurable (eapprox g n).measurable },
id                                                                          
typ                                                                         
st                                                                                          └┘
844      { assume i j h a, exact add_le_add' (monotone_eapprox _ h _) (monotone_eapprox _ h _) }
st                                                                                             └┘
845    end
st     └─┘
846    ... = (⨆n, (eapprox f n).integral) + (⨆n, (eapprox g n).integral) :
id                                                     
typ                                                    
847    by refine (ennreal.supr_add_supr_of_monotone _ _).symm;
848       { assume i j h, exact simple_func.integral_le_integral _ _ (monotone_eapprox _ h) }
st                                                                                          └┘
849    ... = (∫⁻ a, f a) + (∫⁻ a, g a) :
id                             
typ                            
850      by rw [lintegral_eq_supr_eapprox_integral hf, lintegral_eq_supr_eapprox_integral hg]
st                                                                                          
851  
852  @[simp] lemma lintegral_zero : (∫⁻ a:α, 0) = 0 :=
id                                        
typ                                       
doc    └──┘
853  show (∫⁻ a:α, (0 : α →ₛ ennreal) a) = 0, by rw [simple_func.lintegral_eq_integral, zero_integral]
id                         └─────┘  
src                          └─────┘
typ                        └─────┘  
doc                          └─────┘
st                                                                                                   
854  
855  lemma lintegral_finset_sum (s : finset β) {f : β → α → ennreal} (hf : ∀b, measurable (f b)) :
id                                   └┘  └┘               └─────┘                        
src                                  └┘  └┘                 └─────┘
typ                                  └┘  └┘               └─────┘                        
doc                                  └┘  └┘                 └─────┘
856    (∫⁻ a, s.sum (λb, f b a)) = s.sum (λb, ∫⁻ a, f b a) :=
id                                            
typ                                           
857  begin
858    refine finset.induction_on s _ _,
859    { simp },
st            └┘
860    { assume a s has ih,
861      simp [has],
862      rw [lintegral_add (hf _) (measurable_finset_sum s hf), ih] }
id                                                       
typ                                                      
st                                                                 └─
863  end
st   ──┘
864  
865  lemma lintegral_const_mul (r : ennreal) {f : α → ennreal} (hf : measurable f) :
id                                  └─────┘          └─────┘                   
src                                 └─────┘           └─────┘
typ                                 └─────┘          └─────┘                   
doc                                 └─────┘           └─────┘
866    (∫⁻ a, r * f a) = r * (∫⁻ a, f a) :=
id                             
typ                            
867  calc (∫⁻ a, r * f a) = (∫⁻ a, (⨆n, (const α r * eapprox f n) a)) :
id                                                      
typ                                                     
868      by congr; funext a; rw [← supr_eapprox_apply f hf, ennreal.mul_supr]; refl
id                                                                            └──┘
src                                                                            └──┘
typ                                                                           └──┘
doc                                                                            └──┘
869    ... = (⨆n, r * (eapprox f n).integral) :
id                            
typ                           
870    begin
871      rw [lintegral_supr],
872      { congr, funext n, rw [← simple_func.const_mul_integral, ← simple_func.lintegral_eq_integral] },
st                                                                                                    └┘
873      { assume n, exact simple_func.measurable _ },
st                                                  └┘
874      { assume i j h a, exact canonically_ordered_semiring.mul_le_mul (le_refl _)
875          (monotone_eapprox _ h _) }
st                                    └┘
876    end
st     └─┘
877    ... = r * (∫⁻ a, f a) : by rw [← ennreal.mul_supr, lintegral_eq_supr_eapprox_integral hf]
id                     
typ                    
st                                                                                             
878  
879  lemma lintegral_const_mul_le (r : ennreal) (f : α → ennreal) : r * (∫⁻ a, f a) ≤ (∫⁻ a, r * f a) :=
id                                     └─────┘          └─────┘                            
src                                    └─────┘           └─────┘
typ                                    └─────┘          └─────┘                            
doc                                    └─────┘           └─────┘
880  begin
881    rw [lintegral, ennreal.mul_supr],
882    refine supr_le (λs, _),
883    rw [ennreal.mul_supr],
884    simp only [supr_le_iff, ge_iff_le],
885    assume hs,
886    rw ← simple_func.const_mul_integral,
887    refine le_supr_of_le (const α r * s) (le_supr_of_le (λx, _) (le_refl _)),
id                                                         
typ                                                        
888    exact canonically_ordered_semiring.mul_le_mul (le_refl _) (hs x)
id                                                                   
typ                                                                  
889  end
st   └─┘
890  
891  lemma lintegral_const_mul' (r : ennreal) (f : α → ennreal) (hr : r ≠ ⊤) :
id                                   └─────┘          └─────┘        
src                                  └─────┘           └─────┘
typ                                  └─────┘          └─────┘        
doc                                  └─────┘           └─────┘
892    (∫⁻ a, r * f a) = r * (∫⁻ a, f a) :=
id                             
typ                            
893  begin
894    by_cases h : r = 0,
895    { simp [h] },
st                └┘
896    apply le_antisymm _ (lintegral_const_mul_le r f),
id                                                  
typ                                                 
897    have rinv : r * r⁻¹  = 1 := ennreal.mul_inv_cancel h hr,
id                     
typ                    
898    have rinv' : r ⁻¹ * r = 1, by { rw mul_comm, exact rinv },
id                         
typ                        
st                                                             └┘
899    have := lintegral_const_mul_le (r⁻¹) (λx, r * f x),
id                                                 
typ                                                
900    simp [(mul_assoc _ _ _).symm, rinv'] at this,
901    simpa [(mul_assoc _ _ _).symm, rinv]
902      using canonically_ordered_semiring.mul_le_mul (le_refl r) this
903  end
st   └─┘
904  
905  lemma lintegral_supr_const (r : ennreal) {s : set α} (hs : is_measurable s) :
id                                   └─────┘                                
src                                  └─────┘         
typ                                  └─────┘                                
doc                                  └─────┘
906    (∫⁻ a, ⨆(h : a ∈ s), r) = r * volume s :=
id                                     
typ                                    
907  begin
908    rw [← restrict_const_integral r s hs, ← (restrict (const α r) s).lintegral_eq_integral],
909    congr; ext a; by_cases a ∈ s; simp [h, hs]
id                               
typ                              
910  end
st   └─┘
911  
912  lemma lintegral_le_lintegral_ae {f g : α → ennreal} (h : ∀ₘ a, f a ≤ g a) :
id                                             └─────┘                 
src                                             └─────┘
typ                                            └─────┘                 
doc                                             └─────┘
913    (∫⁻ a, f a) ≤ (∫⁻ a, g a) :=
id                       
typ                      
914  begin
915    rcases exists_is_measurable_superset_of_measure_eq_zero h with ⟨t, hts, ht, ht0⟩,
916    have : - t ∈ (@measure_space.μ α _).a_e,
id                                   
typ                                  
917    { rw [measure.mem_a_e_iff, lattice.neg_neg, ht0] },
st                                                     └┘
918    refine (supr_le $ assume s, supr_le $ assume hfs,
919      le_supr_of_le (s.restrict (- t)) $ le_supr_of_le _ _),
id                                    
typ                                   
920    { assume a,
921      by_cases a ∈ t;
id                   
typ                  
922        simp [h, simple_func.restrict_apply, ht.compl],
923      exact le_trans (hfs a) (by_contradiction $ assume hnfg, h (hts hnfg)) },
id                           
typ                          
st                                                                             └┘
924    { refine le_of_eq (s.integral_congr _ _),
925      filter_upwards [this],
926      refine assume a hnt, _,
id                     
typ                    
927      by_cases hat : a ∈ t; simp [hat, ht.compl],
id                         
typ                        
928      exact (hnt hat).elim }
st                            └─
929  end
st   ──┘
930  
931  lemma lintegral_congr_ae {f g : α → ennreal} (h : ∀ₘ a, f a = g a) :
id                                      └─────┘                  
src                                      └─────┘
typ                                     └─────┘                  
doc                                      └─────┘
932    (∫⁻ a, f a) = (∫⁻ a, g a) :=
id                       
typ                      
933  le_antisymm
934    (lintegral_le_lintegral_ae $ by filter_upwards [h] assume a h, le_of_eq h)
id                                                               
typ                                                              
935    (lintegral_le_lintegral_ae $ by filter_upwards [h] assume a h, le_of_eq h.symm)
id                                                               
typ                                                              
936  
937  -- TODO: Need a better way of rewriting inside of a integral
938  lemma lintegral_rw₁ {f f' : α → β} (h : ∀ₘ a, f a = f' a) (g : β → ennreal) :
id                                                  └┘            └─────┘
src                                                                     └─────┘
typ                                                 └┘            └─────┘
doc                                                                     └─────┘
939    (∫⁻ a, g (f a)) = (∫⁻ a, g (f' a)) :=
id                              
typ                             
940  begin
941    apply lintegral_congr_ae,
942    filter_upwards [h],
943    assume a,
944    simp only [mem_set_of_eq],
945    assume h,
946    rw h
947  end
st   └─┘
948  
949  -- TODO: Need a better way of rewriting inside of a integral
950  lemma lintegral_rw₂ {f₁ f₁' : α → β} {f₂ f₂' : α → γ} (h₁ : ∀ₘ a, f₁ a = f₁' a)
id                                                                └┘    └─┘ 
typ                                                               └┘    └─┘ 
951    (h₂ : ∀ₘ a, f₂ a = f₂' a) (g : β → γ → ennreal) :
id                └┘                    └─────┘
src                                           └─────┘
typ               └┘                    └─────┘
doc                                           └─────┘
952    (∫⁻ a, g (f₁ a) (f₂ a)) = (∫⁻ a, g (f₁' a) (f₂' a)) :=
id             └┘    └┘              └─┘    └─┘ 
typ            └┘    └┘              └─┘    └─┘ 
953  begin
954    apply lintegral_congr_ae,
955    filter_upwards [h₁, h₂],
956    assume a,
957    simp only [mem_set_of_eq],
958    repeat { assume h, rw h }
959  end
st   └─┘
960  
961  lemma simple_func.lintegral_map (f : α →ₛ β) (g : β → ennreal) :
id                                                      └─────┘
src                                                        └─────┘
typ                                                     └─────┘
doc                                                        └─────┘
962    (∫⁻ a, (f.map g) a) = ∫⁻ a, g (f a) :=
id                                 
typ                                
963  by { apply lintegral_congr_ae, filter_upwards [], assume a, exact map_apply _ _ _ }
st                                                                                     └┘
964  
965  lemma lintegral_eq_zero_iff {f : α → ennreal} (hf : measurable f) :
id                                       └─────┘                   
src                                       └─────┘
typ                                      └─────┘                   
doc                                       └─────┘
966    lintegral f = 0 ↔ (∀ₘ a, f a = 0) :=
id                            
src                    
typ                           
967  begin
968    refine iff.intro (assume h, _) (assume h, _),
969    { have : ∀n:ℕ, ∀ₘ a, f a < n⁻¹,
id                         
typ                        
970      { assume n,
971        have : is_measurable {a : α | f a ≥ n⁻¹ },
id                                           
typ                                          
972        { exact hf _ (is_measurable_of_is_closed $ is_closed_ge' _) },
st                                                                     └┘
973        have : (n : ennreal)⁻¹ * volume {a | f a ≥ n⁻¹ } = 0,
id                     └─────┘                      
src                    └─────┘
typ                    └─────┘                      
doc                    └─────┘
974        { rw [← simple_func.restrict_const_integral _ _ this, ← le_zero_iff_eq,
975            ← simple_func.lintegral_eq_integral],
976          refine le_trans (lintegral_le_lintegral _ _ _) (le_of_eq h),
977          assume a, by_cases h : (n : ennreal)⁻¹ ≤ f a; simp [h, (≥), this] },
id                                      └─────┘       
src                                      └─────┘
typ                                     └─────┘       
doc                                      └─────┘
st                                                                             └┘
978        rw [ennreal.mul_eq_zero, ennreal.inv_eq_zero] at this,
979        simpa [ennreal.nat_ne_top, all_ae_iff] using this },
st                                                           └┘
980      filter_upwards [all_ae_all_iff.2 this],
981      dsimp,
982      assume a ha,
983      by_contradiction h,
984      rcases ennreal.exists_inv_nat_lt h with ⟨n, hn⟩,
985      exact (lt_irrefl _ $ lt_trans hn $ ha n).elim },
id                                             
typ                                            
st                                                     └┘
986    { calc lintegral f = lintegral (λa:α, 0) : lintegral_congr_ae h
id                                       
typ                                      
987        ... = 0 : lintegral_zero }
st                                  └─
988  end
st   ──┘
989  
990  /-- Weaker version of the monotone convergence theorem-/
991  lemma lintegral_supr_ae {f : ℕ → α → ennreal} (hf : ∀n, measurable (f n))
id                                      └─────┘                         
src                                      └─────┘
typ                                     └─────┘                         
doc                                       └─────┘
992    (h_mono : ∀n, ∀ₘ a, f n a ≤ f n.succ a) :
id                             └──┘  
src                                   └──┘
typ                            └──┘  
993    (∫⁻ a, ⨆n, f n a) = (⨆n, ∫⁻ a, f n a) :=
id                                
typ                               
994  let ⟨s, hs⟩ := exists_is_measurable_superset_of_measure_eq_zero
id        
typ       
995                         (all_ae_iff.1 (all_ae_all_iff.2 h_mono)) in
996  let g := λ n a, if a ∈ s then 0 else f n a in
id                                      
typ                                     
997  have g_eq_f : ∀ₘ a, ∀n, g n a = f n a,
id                                  
typ                                 
998    begin
999      have := hs.2.2, rw [← compl_compl s] at this,
id                                         
typ                                        
1000      filter_upwards [(measure.mem_a_e_iff (-s)).2 this] assume a ha n, if_neg ha
id                                                                    
typ                                                                   
1001    end,
st     └─┘
1002  calc
1003    (∫⁻ a, ⨆n, f n a) = (∫⁻ a, ⨆n, g n a) :
id                                
typ                               
1004    lintegral_congr_ae
1005      begin
1006        filter_upwards [g_eq_f], assume a ha, congr, funext, exact (ha n).symm
id                                                                        
typ                                                                       
1007      end
st       └─┘
1008    ... = ⨆n, (∫⁻ a, g n a) :
id                       
typ                      
1009    lintegral_supr
1010      (assume n, measurable.if hs.2.1 measurable_const (hf n))
id                                                           
typ                                                          
1011      (monotone_of_monotone_nat $ assume n a,  classical.by_cases
id                                           
typ                                          
1012        (assume h : a ∈ s, by simp [g, if_pos h])
id                                    
typ                                   
1013        (assume h : a ∉ s,
id                     
typ                    
1014        begin
1015          simp only [g, if_neg h], have := hs.1, rw subset_def at this, have := mt (this a) h,
id                                                                                         
typ                                                                                        
1016          simp only [not_not, mem_set_of_eq] at this, exact this n
id                                                                  
typ                                                                 
1017        end))
st         └─┘
1018    ... = ⨆n, (∫⁻ a, f n a) :
id                      
typ                     
1019    begin
1020      congr, funext, apply lintegral_congr_ae, filter_upwards [g_eq_f] assume a ha, ha n
id                                                                                       
typ                                                                                      
1021    end
st     └─┘
1022  
1023  lemma lintegral_sub {f g : α → ennreal} (hf : measurable f) (hg : measurable g)
id                                 └─────┘                                      
src                                 └─────┘
typ                                └─────┘                                      
doc                                 └─────┘
1024    (hg_fin : lintegral g < ⊤) (h_le : ∀ₘ a, g a ≤ f a) :
id                                                 
typ                                                
1025    (∫⁻ a, f a - g a) = (∫⁻ a, f a) - (∫⁻ a, g a) :=
id                                      
typ                                     
1026  begin
1027    rw [← ennreal.add_right_inj hg_fin,
1028          ennreal.sub_add_cancel_of_le (lintegral_le_lintegral_ae h_le),
1029        ← lintegral_add (ennreal.measurable.sub hf hg) hg],
1030    show  (∫⁻ (a : α), f a - g a + g a) = ∫⁻ (a : α), f a,
id                                                     
typ                                                    
1031    apply lintegral_congr_ae, filter_upwards [h_le], simp only [add_comm, mem_set_of_eq],
1032    assume a ha, exact ennreal.add_sub_cancel_of_le ha
1033  end
st   └─┘
1034  
1035  /-- Monotone convergence theorem for nonincreasing sequences of functions -/
1036  lemma lintegral_infi_ae
1037    {f : ℕ → α → ennreal} (h_meas : ∀n, measurable (f n))
id                └─────┘                            
src                └─────┘
typ               └─────┘                            
doc                 └─────┘
1038    (h_mono : ∀n:ℕ, ∀ₘ a, f n.succ a ≤ f n a) (h_fin : lintegral (f 0) < ⊤) :
id                          └───┘      
src                            └───┘
typ                         └───┘      
1039    (∫⁻ a, ⨅n, f n a) = (⨅n, ∫⁻ a, f n a) :=
id                                 
typ                                
1040  have fn_le_f0 : (∫⁻ a, ⨅n, f n a) ≤ lintegral (f 0), from
id                                              
typ                                             
1041    lintegral_le_lintegral _ _ (assume a, infi_le_of_le 0 (le_refl _)),
id                                        
typ                                       
1042  have fn_le_f0' : (⨅n, ∫⁻ a, f n a) ≤ lintegral (f 0), from infi_le_of_le 0 (le_refl _),
id                                               
typ                                              
1043  (ennreal.sub_left_inj h_fin fn_le_f0 fn_le_f0').1 $
1044  show lintegral (f 0) - (∫⁻ a, ⨅n, f n a) = lintegral (f 0) - (⨅n, ∫⁻ a, f n a), from
id                                                                    
typ                                                                   
1045  calc
1046    lintegral (f 0) - (∫⁻ a, ⨅n, f n a) = ∫⁻ a, f 0 a - ⨅n, f n a :
id                                                       
typ                                                      
1047      (lintegral_sub (h_meas 0) (measurable.infi h_meas)
1048      (calc
1049        (∫⁻ a, ⨅n, f n a)  ≤ lintegral (f 0) : lintegral_le_lintegral _ _
id                                    
typ                                   
1050                                               (assume a, infi_le _ _)
id                                                        
typ                                                       
1051            ... < ⊤ : h_fin  )
1052      (all_ae_of_all $ assume a, infi_le _ _)).symm
id                               
typ                              
1053    ... = ∫⁻ a, ⨆n, f 0 a - f n a : congr rfl (funext (assume a, ennreal.sub_infi))
id                                                          
typ                                                         
1054    ... = ⨆n, ∫⁻ a, f 0 a - f n a :
id                             
typ                            
1055      lintegral_supr_ae
1056        (assume n, ennreal.measurable.sub (h_meas 0) (h_meas n))
id                                                             
typ                                                            
1057        (assume n, by
id                 
typ                
1058          filter_upwards [h_mono n] assume a ha, ennreal.sub_le_sub (le_refl _) ha)
id                                           
typ                                          
1059    ... = ⨆n, lintegral (f 0) - ∫⁻ a, f n a :
id                                        
typ                                       
1060      have h_mono : ∀ₘ a, ∀n:ℕ, f n.succ a ≤ f n a := all_ae_all_iff.2 h_mono,
id                                └───┘      
src                                  └───┘
typ                               └───┘      
1061      have h_mono : ∀n, ∀ₘa, f n a ≤ f 0 a := assume n,
id                                               
typ                                              
1062      begin
1063        filter_upwards [h_mono], simp only [mem_set_of_eq], assume a, assume h, induction n with n ih,
id                                                                                           
typ                                                                                          
1064        {exact le_refl _}, {exact le_trans (h n) ih}
id                                               
typ                                              
st                         └┘                         └┘
1065      end,
st       └─┘
1066      congr rfl (funext $ assume n, lintegral_sub (h_meas _) (h_meas _)
id                                  
typ                                 
1067        (calc
1068          (∫⁻ a, f n a) ≤ ∫⁻ a, f 0 a : lintegral_le_lintegral_ae $ h_mono n
id                                                                     
typ                                                                    
1069          ... < ⊤ : h_fin)
1070          (h_mono n))
id                   
typ                  
1071    ... = lintegral (f 0) - (⨅n, ∫⁻ a, f n a) : ennreal.sub_infi.symm
id                                       
typ                                      
1072  
1073  section priority
1074  -- for some reason the next proof fails without changing the priority of this instance
1075  local attribute [instance, priority 1000] classical.prop_decidable
id                                             └──────────────────────┘
src                                            └──────────────────────┘
typ                                            └──────────────────────┘
1076  /-- Known as Fatou's lemma -/
1077  lemma lintegral_liminf_le {f : ℕ → α → ennreal} (h_meas : ∀n, measurable (f n)) :
id                                        └─────┘               └────────┘   
src                                        └─────┘                └────────┘
typ                                       └─────┘               └────────┘   
doc                                         └─────┘                └────────┘
1078    (∫⁻ a, liminf at_top (λ n, f n a)) ≤ liminf at_top (λ n, lintegral (f n)) :=
id      └┘  └────┘ └────┘            └────┘ └────┘      └───────┘   
src     └┘   └────┘ └────┘                └────┘ └────┘       └───────┘
typ     └┘  └────┘ └────┘            └────┘ └────┘      └───────┘   
doc     └┘          └────┘                        └────┘       └───────┘
1079  calc
1080    (∫⁻ a, liminf at_top (λ n, f n a)) = ∫⁻ a, ⨆n:ℕ, ⨅i≥n, f i a :
id      └┘  └────┘ └────┘             └┘         
src     └┘   └────┘ └────┘                 └┘         
typ     └┘  └────┘ └────┘             └┘         
doc     └┘          └────┘                 └┘          
1081       congr rfl (funext (assume a, liminf_eq_supr_infi_of_nat))
id        └───┘ └─┘  └────┘           └────────────────────────┘
src       └───┘ └─┘  └────┘            └────────────────────────┘
typ       └───┘ └─┘  └────┘           └────────────────────────┘
1082    ... = ⨆n:ℕ, ∫⁻ a, ⨅i≥n, f i a :
id              └┘      
src             └┘      
typ             └┘      
doc              └┘      
1083      lintegral_supr
id       └────────────┘
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
1084      begin
st       └─────
1085        assume n, apply measurable.infi, assume i, by_cases h : i ≥ n,
id                                                                    
typ                                                                   
st   ─────┘         
1086        {convert h_meas i, simp [h]},
id                                 
typ                                
st                                    └┘
1087        {convert measurable_const, simp [h]}
id                                          
typ                                         
st                                            └┘
1088      end
st       └─┘
1089      begin
1090        assume n m hnm a, simp only [le_infi_iff], assume i hi,
1091        refine infi_le_of_le i (infi_le_of_le (le_trans hnm hi) (le_refl _))
id                                                            └┘
typ                                                           └┘
1092      end
st       └─┘
1093    ... ≤ ⨆n:ℕ, ⨅i≥n, lintegral (f i) :
id                                 
src             
typ                                
1094      supr_le_supr $ assume n, le_infi $
id                             
typ                            
1095        assume i, le_infi $ assume hi, lintegral_le_lintegral _ _
id                                   └┘
typ                                  └┘
1096        $ assume a, infi_le_of_le i $ infi_le_of_le hi $ le_refl _
id                                                   └┘
typ                                                  └┘
1097    ... = liminf at_top (λ n, lintegral (f n)) : liminf_eq_supr_infi_of_nat.symm
id                                          
typ                                         
1098  end priority
1099  
1100  lemma limsup_lintegral_le {f : ℕ → α → ennreal} {g : α → ennreal}
id                                        └─────┘          └─────┘
src                                        └─────┘           └─────┘
typ                                       └─────┘          └─────┘
doc                                         └─────┘           └─────┘
1101    (hf_meas : ∀ n, measurable (f n)) (h_bound : ∀n, ∀ₘa, f n a ≤ g a) (h_fin : lintegral g < ⊤) :
id                                                                                 
typ                                                                                
1102    limsup at_top (λn, lintegral (f n)) ≤ ∫⁻ a, limsup at_top (λn, f n a) :=
id                                                                  
typ                                                                 
1103  calc
1104    limsup at_top (λn, lintegral (f n)) = ⨅n:ℕ, ⨆i≥n, lintegral (f i) :
id                                                              
src                                             
typ                                                             
1105      limsup_eq_infi_supr_of_nat
1106    ... ≤ ⨅n:ℕ, ∫⁻ a, ⨆i≥n, f i a :
id                            
src             
typ                           
1107      infi_le_infi $ assume n, supr_le $ assume i, supr_le $ assume hi,
id                                                                   └┘
typ                                                                  └┘
1108      lintegral_le_lintegral _ _ $ assume a, le_supr_of_le i $ le_supr_of_le hi (le_refl _)
id                                                                            └┘
typ                                                                           └┘
1109    ... = ∫⁻ a, ⨅n:ℕ, ⨆i≥n, f i a :
id                            
src                   
typ                           
1110      (lintegral_infi_ae
1111        (assume n,
id                 
typ                
1112             @measurable.supr _ _ _ _ _ _ _ _ _ (λ i a, supr (λ (h : i ≥ n), f i a))
id                                                                            
typ                                                                           
1113        (assume i, measurable.supr_Prop (hf_meas i)))
id                                                 
typ                                                
1114        (assume n, all_ae_of_all $ assume a,
id                                          
typ                                         
1115         begin
1116           simp only [supr_le_iff], assume i hi, refine le_supr_of_le i _,
id                                                                       
typ                                                                      
1117           rw [supr_pos _], exact le_refl _, exact nat.le_of_succ_le hi
id                                                                      └┘
typ                                                                     └┘
1118         end )
st          └─┘
1119        (lt_of_le_of_lt
1120          (lintegral_le_lintegral_ae
1121          begin
1122            filter_upwards [all_ae_all_iff.2 h_bound],
1123            simp only [supr_le_iff, mem_set_of_eq],
1124            assume a ha i hi, exact ha i
id                                        
typ                                       
1125          end )
st           └─┘
1126          h_fin)).symm
1127    ... = ∫⁻ a, limsup at_top (λn, f n a) :
id                                    
typ                                   
1128      lintegral_congr_ae $ all_ae_of_all $ assume a, limsup_eq_infi_supr_of_nat.symm
id                                                   
typ                                                  
1129  
1130  /-- Dominated convergence theorem for nonnegative functions -/
1131  lemma tendsto_lintegral_of_dominated_convergence
1132    {F : ℕ → α → ennreal} {f : α → ennreal} (bound : α → ennreal)
id                └─────┘           └─────┘              └─────┘
src                └─────┘           └─────┘               └─────┘
typ               └─────┘           └─────┘              └─────┘
doc                 └─────┘           └─────┘               └─────┘
1133    (hF_meas : ∀n, measurable (F n)) (h_bound : ∀n, ∀ₘ a, F n a ≤ bound a)
id                                                           └───┘ 
typ                                                          └───┘ 
1134    (h_fin : lintegral bound < ⊤)
id                         └┘
typ                        └┘
1135    (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id                                                 
typ                                                
1136    tendsto (λn, lintegral (F n)) at_top (𝓝 (lintegral f)) :=
id                             
typ                            
1137  begin
1138    have limsup_le_lintegral :=
1139    calc
1140      limsup at_top (λ (n : ℕ), lintegral (F n)) ≤ ∫⁻ (a : α), limsup at_top (λn, F n a) :
id                                                                               
typ                                                                              
1141        limsup_lintegral_le hF_meas h_bound h_fin
1142      ... = lintegral f :
id                       
typ                      
1143        lintegral_congr_ae $
1144            by filter_upwards [h_lim] assume a h, limsup_eq_of_tendsto at_top_ne_bot h,
id                                              
typ                                             
1145    have lintegral_le_liminf :=
1146    calc
1147      lintegral f = ∫⁻ (a : α), liminf at_top (λ (n : ℕ), F n a) :
id                            
typ                           
1148        lintegral_congr_ae $
1149        by filter_upwards [h_lim] assume a h, (liminf_eq_of_tendsto at_top_ne_bot h).symm
id                                          
typ                                         
1150      ... ≤ liminf at_top (λ n, lintegral (F n)) :
id                              
typ                             
1151        lintegral_liminf_le hF_meas,
1152    have liminf_eq_limsup :=
1153      le_antisymm
1154        (liminf_le_limsup (map_ne_bot at_top_ne_bot))
1155        (le_trans limsup_le_lintegral lintegral_le_liminf),
1156    have liminf_eq_lintegral : liminf at_top (λ n, lintegral (F n)) = lintegral f :=
id                                                                               
typ                                                                              
1157      le_antisymm (by convert limsup_le_lintegral) lintegral_le_liminf,
1158    have limsup_eq_lintegral : limsup at_top (λ n, lintegral (F n)) = lintegral f :=
id                                                                               
typ                                                                              
1159      le_antisymm
1160        limsup_le_lintegral
1161        begin convert lintegral_le_liminf, exact liminf_eq_limsup.symm end,
st                                                                        └─┘
1162    exact tendsto_of_liminf_eq_limsup ⟨liminf_eq_lintegral, limsup_eq_lintegral⟩
1163  end
st   └─┘
1164  
1165  /-- Dominated convergence theorem for filters with a countable basis -/
1166  lemma tendsto_lintegral_filter_of_dominated_convergence {ι} {l : filter ι}
id                                                                      └┘   
src                                                                     └┘
typ                                                                     └┘   
1167    {F : ι → α → ennreal} {f : α → ennreal} (bound : α → ennreal)
id                └─────┘          └─────┘              └─────┘
src                 └─────┘           └─────┘               └─────┘
typ               └─────┘          └─────┘              └─────┘
doc                 └─────┘           └─────┘               └─────┘
1168    (hl_cb : l.has_countable_basis)
1169    (hF_meas : ∀ᶠ n in l, measurable (F n))
id                                      
typ                                     
1170    (h_bound : ∀ᶠ n in l, ∀ₘ a, F n a ≤ bound a)
id                                   └───┘ 
typ                                  └───┘ 
1171    (h_fin : lintegral bound < ⊤)
id                         └─┘
typ                        └─┘
1172    (h_lim : ∀ₘ a, tendsto (λ n, F n a) l (nhds (f a))) :
id                                              
typ                                             
1173    tendsto (λn, lintegral (F n)) l (nhds (lintegral f)) :=
id                                
typ                               
1174  begin
1175    rw hl_cb.tendsto_iff_seq_tendsto,
1176    { intros x xl,
1177      have hxl, { rw tendsto_at_top' at xl, exact xl },
st                                                      └┘
1178      have h := inter_mem_sets hF_meas h_bound,
1179      replace h := hxl _ h,
1180      rcases h with ⟨k, h⟩,
1181      rw ← tendsto_add_at_top_iff_nat k,
id                                       
typ                                      
1182      refine tendsto_lintegral_of_dominated_convergence _ _ _ _ _,
1183      { exact bound },
id               └───┘
typ              └───┘
st                     └┘
1184      { intro, refine (h _ _).1, exact nat.le_add_left _ _ },
st                                                            └┘
1185      { intro, refine (h _ _).2, exact nat.le_add_left _ _ },
st                                                            └┘
1186      { assumption },
st                    └┘
1187      { filter_upwards [h_lim],
1188        simp only [mem_set_of_eq],
1189        assume a h_lim,
1190        apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
id                                                       
typ                                                      
1191        { assumption },
st                      └┘
1192        rw tendsto_add_at_top_iff_nat,
1193        assumption } },
st                    └──┘
1194  end
st   └─┘
1195  
1196  section
1197  open encodable
1198  
1199  /-- Monotone convergence for a suprema over a directed family and indexed by an encodable type -/
1200  theorem lintegral_supr_directed [encodable β] {f : β → α → ennreal}
id                                    └┘  └──┘                └───┘
src                                   └┘  └──┘                   └───┘
typ                                   └┘  └──┘                └───┘
doc                                   └┘  └──┘                   └───┘
1201    (hf : ∀b, measurable (f b)) (h_directed : directed (≤) f) :
id                                                          
typ                                                         
1202    (∫⁻ a, ⨆b, f b a) = (⨆b, ∫⁻ a, f b a) :=
id                               
typ                              
1203  begin
1204    by_cases hβ : ¬ nonempty β,
id                    └──────┘ 
src                   └──────┘
typ                   └──────┘ 
1205    { have : ∀f : β → ennreal, (⨆(b : β), f b) = 0 :=
id                      └─────┘         
src                      └─────┘
typ                     └─────┘         
doc                      └─────┘
1206        assume f, supr_eq_bot.2 (assume b, (hβ ⟨b⟩).elim),
id                                           └┘
typ                                          └┘
1207      simp [this] },
st                   └┘
1208    cases of_not_not hβ with b,
id                      └┘
typ                     └┘
1209    haveI iβ : inhabited β := ⟨b⟩, clear hβ b,
id                └───────┘      
src               └───────┘
typ               └───────┘      
1210    have : ∀a, (⨆ b, f b a) = (⨆ n, f (h_directed.sequence f n) a),
id                                
typ                               
1211    { assume a,
1212      refine le_antisymm (supr_le $ assume b, _) (supr_le $ assume n, le_supr (λn, f n a) _),
id                                                                                    
typ                                                                                   
1213      exact le_supr_of_le (encode b + 1) (h_directed.le_sequence b a) },
id                                                                   
typ                                                                  
st                                                                       └┘
1214    calc (∫⁻ a, ⨆ b, f b a) = (∫⁻ a, ⨆ n, f (h_directed.sequence f n) a) :
id                                     
typ                                    
1215        by simp only [this]
1216      ... = (⨆ n, ∫⁻ a, f (h_directed.sequence f n) a) :
id                     
typ                    
1217        lintegral_supr (assume n, hf _) h_directed.sequence_mono
id                                
typ                               
1218      ... = (⨆ b, ∫⁻ a, f b a) :
id                     
typ                    
1219      begin
1220        refine le_antisymm (supr_le $ assume n, _) (supr_le $ assume b, _),
id                                                                     
typ                                                                    
1221        { exact le_supr (λb, lintegral (f b)) _ },
id                                        
typ                                       
st                                                 └┘
1222        { exact le_supr_of_le (encode b + 1)
1223            (lintegral_le_lintegral _ _ $ h_directed.le_sequence b) }
id                                                                  
typ                                                                 
st                                                                     └┘
1224      end
st       └─┘
1225  end
st   └─┘
1226  
1227  end
1228  
1229  lemma lintegral_tsum [encodable β] {f : β → α → ennreal} (hf : ∀i, measurable (f i)) :
id                         └──┘  └─┘               └─────┘                        
src                        └──┘  └─┘                 └─────┘
typ                        └──┘  └─┘               └─────┘                        
doc                        └──┘  └─┘                 └─────┘
1230    (∫⁻ a, ∑ i, f i a) = (∑ i, ∫⁻ a, f i a) :=
id                                 
typ                                
1231  begin
1232    simp only [ennreal.tsum_eq_supr_sum],
1233    rw [lintegral_supr_directed],
1234    { simp [lintegral_finset_sum _ hf] },
st                                        └┘
1235    { assume b, exact measurable_finset_sum _ hf },
st                                                  └┘
1236    { assume s t,
1237      use [s ∪ t],
id               
typ              
1238      split,
1239      exact assume a, finset.sum_le_sum_of_subset (finset.subset_union_left _ _),
id                    
typ                   
1240      exact assume a, finset.sum_le_sum_of_subset (finset.subset_union_right _ _) }
id                    
typ                   
st                                                                                   └─
1241  end
st   ──┘
1242  
1243  end lintegral
1244  
1245  namespace measure
1246  
1247  def integral [measurable_space α] (m : measure α) (f : α → ennreal) : ennreal :=
id                 └┘  └──┘  └──┘                            └─────┘    └─────┘
src                └┘  └──┘  └──┘                               └─────┘    └─────┘
typ                └┘  └──┘  └──┘                            └─────┘    └─────┘
doc                                                             └─────┘    └─────┘
1248  @lintegral α { μ := m } f
id                      
typ                     
1249  
1250  variables [measurable_space α] {m : measure α}
id              └┘ └┘ └┘ └┘ └┘ 
src             └┘ └┘ └┘ └┘ └┘ 
typ             └┘ └┘ └┘ └┘ └┘ 
1251  
1252  @[simp] lemma integral_zero : m.integral (λa, 0) = 0 := @lintegral_zero α { μ := m }
id                                                                                  
typ                                                                                 
doc    └──┘
1253  
1254  lemma integral_map [measurable_space β] {f : β → ennreal} {g : α → β}
id                       └──┘  └──┘  └──┘            └─┘ └─┘          
src                      └──┘  └──┘  └──┘             └─┘ └─┘
typ                      └──┘  └──┘  └──┘            └─┘ └─┘          
doc                                                   └─┘ └─┘
1255    (hf : measurable f) (hg : measurable g) : (map g m).integral f = m.integral (f ∘ g) :=
id                                                                               
typ                                                                              
1256  begin
1257    rw [integral, integral, lintegral_eq_supr_eapprox_integral, lintegral_eq_supr_eapprox_integral],
1258    { congr, funext n, symmetry,
1259      apply simple_func.integral_map,
1260      { assume a, exact congr_fun (simple_func.eapprox_comp hf hg) a },
id                                                                    
typ                                                                   
st                                                                      └┘
1261      { assume s hs, exact map_apply hg hs } },
st                                            └──┘
1262    exact hf.comp hg,
1263    assumption
1264  end
st   └─┘
1265  
1266  lemma integral_dirac (a : α) {f : α → ennreal} (hf : measurable f) : (dirac a).integral f = f a :=
id                                       └─────┘                                             
src                                        └─────┘
typ                                      └─────┘                                             
doc                                        └─────┘
1267  have ∀f:α →ₛ ennreal, @simple_func.integral α {μ := dirac a} f = f a,
id               └─────┘                                           
src               └─────┘
typ              └─────┘                                           
doc               └─────┘
1268  begin
1269    assume f,
1270    have : ∀r, @volume α { μ := dirac a } (⇑f ⁻¹' {r}) = ⨆ h : f a = r, 1,
id                                                                
typ                                                               
1271    { assume r,
1272      transitivity,
1273      apply dirac_apply,
1274      apply simple_func.measurable_sn,
1275      refine supr_congr_Prop _ _; simp },
st                                        └┘
1276    transitivity,
1277    apply finset.sum_eq_single (f a),
id                                  
typ                                 
1278    { assume b hb h, simp [this, ne.symm h], },
st                                              └┘
1279    { assume h, simp at h, exact (h a rfl).elim },
id                                     
typ                                    
st                                                 └┘
1280    { rw [this], simp }
st                       └─
1281  end,
st   ──┘
1282  begin
1283    rw [integral, lintegral_eq_supr_eapprox_integral],
1284    { simp [this, simple_func.supr_eapprox_apply f hf] },
id                                                  
typ                                                 
st                                                        └┘
1285    assumption
1286  end
st   └─┘
1287  
1288  def with_density (m : measure α) (f : α → ennreal) : measure α :=
id                                           └─────┘            
src                                            └─────┘
typ                                          └─────┘            
doc                                            └─────┘
1289  if hf : measurable f then
id                      
typ                     
1290    measure.of_measurable (λs hs, m.integral (λa, ⨆(h : a ∈ s), f a))
id                                                            
typ                                                           
1291      (by simp)
1292      begin
1293        assume s hs hd,
1294        have : ∀a, (⨆ (h : a ∈ ⋃i, s i), f a) = (∑i, (⨆ (h : a ∈ s i), f a)),
id                                                                     
typ                                                                    
1295        { assume a,
1296          by_cases ha : ∃j, a ∈ s j,
id                               
typ                              
1297          { rcases ha with ⟨j, haj⟩,
1298            have : ∀i, a ∈ s i ↔ j = i := assume i,
id                                              
typ                                             
1299              iff.intro
1300                (assume hai, by_contradiction $ assume hij, hd j i hij ⟨haj, hai⟩)
id                                                        └─┘     
typ                                                       └─┘     
1301                (by rintros rfl; assumption),
id                                  └────────┘
src                                 └────────┘
typ                                 └────────┘
doc                                 └────────┘
1302            simp [this, ennreal.tsum_supr_eq] },
st                                               └┘
1303          { have : ∀i, ¬ a ∈ s i, { simpa using ha },
id                            
typ                           
st                                                    └┘
1304            simp [this] } },
st                         └──┘
1305        simp only [this],
1306        apply lintegral_tsum,
1307        { assume i,
1308          simp [supr_eq_if],
1309          exact measurable.if (hs i) hf measurable_const }
id                                   
typ                                  
st                                                          └┘
1310      end
st       └─┘
1311  else 0
1312  
1313  lemma with_density_apply {m : measure α} {f : α → ennreal} {s : set α}
id                                                   └─────┘         
src                                                    └─────┘         
typ                                                  └─────┘         
doc                                                    └─────┘
1314    (hf : measurable f) (hs : is_measurable s) :
id                                            
typ                                           
1315    m.with_density f s = m.integral (λa, ⨆(h : a ∈ s), f a) :=
id                                                  
typ                                                 
1316  by rw [with_density, dif_pos hf]; exact measure.of_measurable_apply s hs
id                                                                        └┘
typ                                                                       └┘
1317  
1318  end measure
1319  
1320  end measure_theory